Theorems · Theorem · probability

IicProdIoc_preimage

∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  [inst_3 : LocallyFiniteOrderBot ι] {a b : ι} (hab : a ≤ b) (s : (i : ↥(Finset.Iic b)) → Set (X ↑i)),
  IicProdIoc a b ⁻¹' Set.univ.pi s = Set.univ.pi (Preorder.frestrictLe₂ hab s) ×ˢ Set.univ.pi (Finset.restrict₂ ⋯ s)

Defined in: Mathlib.Probability.Kernel.IonescuTulcea.Maps
Cited by: 1 results in Mathlib
Foundations: Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: LinearOrder LocallyFiniteOrder DecidableLE LocallyFiniteOrderBot

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites21

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Finsetstatement · cited by 13,712
LinearOrderstatement and proof · cited by 8,572
Set.preimagestatement · cited by 4,946
Set.univstatement · cited by 3,945
LE.le.transproof · cited by 3,151
Set.extproof · cited by 2,266
SProd.sprodstatement · cited by 1,750
LocallyFiniteOrderstatement and proof · cited by 658
Set.pistatement · cited by 405
not_leproof · cited by 328
Finset.Iocstatement and proof · cited by 301

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.Measure.pi_prod_map_IicProdIocproof · cited by 1