Maps

📁 Source: Mathlib/Probability/Kernel/IonescuTulcea/Maps.lean

Statistics

Metric	Count
Definitions IicProdIoc, IocProdIoc, IicProdIoc, IicProdIoi, piSingleton	5
Theorems IicProdIoc_comp_restrict₂, IicProdIoc_def, IicProdIoc_le, IicProdIoc_preimage, IicProdIoc_self, IocProdIoc_preimage, coe_IicProdIoc, coe_IicProdIoc_symm, frestrictLe₂_comp_IicProdIoc, measurable_IicProdIoc, measurable_IocProdIoc, restrict₂_comp_IicProdIoc	12
Total	17

MeasurableEquiv

Definitions

Name	Category	Theorems
IicProdIoc 📖	CompOp	2 math math: coe_IicProdIoc_symm, coe_IicProdIoc
IicProdIoi 📖	CompOp	1 math math: ProbabilityTheory.Kernel.traj_eq_prod
piSingleton 📖	CompOp	4 math math: ProbabilityTheory.Kernel.partialTraj_succ_of_le, MeasureTheory.Measure.map_piSingleton, ProbabilityTheory.Kernel.partialTraj_le_def, ProbabilityTheory.Kernel.partialTraj_succ_self

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_IicProdIoc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	DFunLike.coe MeasurableEquiv Prod.instMeasurableSpace MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Finset.Ioc EquivLike.toFunLike instEquivLike IicProdIoc IicProdIoc	—	—
coe_IicProdIoc_symm 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	DFunLike.coe MeasurableEquiv MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Prod.instMeasurableSpace Finset.Ioc EquivLike.toFunLike instEquivLike symm IicProdIoc Preorder.frestrictLe₂ Finset.restrict₂ Finset.Ioc_subset_Iic_self	—	—

(root)

Definitions

Name	Category	Theorems
IicProdIoc 📖	CompOp	15 math math: ProbabilityTheory.Kernel.partialTraj_succ_of_le, ProbabilityTheory.Kernel.partialTraj_le_def, IicProdIoc_def, MeasureTheory.Measure.pi_prod_map_IicProdIoc, MeasureTheory.partialTraj_const, ProbabilityTheory.Kernel.partialTraj_succ_self, measurable_IicProdIoc, MeasurableEquiv.coe_IicProdIoc, IicProdIoc_preimage, IicProdIoc_self, frestrictLe₂_comp_IicProdIoc, IicProdIoc_comp_restrict₂, IicProdIoc_le, ProbabilityTheory.Kernel.partialTraj_eq_prod, restrict₂_comp_IicProdIoc
IocProdIoc 📖	CompOp	3 math math: IocProdIoc_preimage, MeasureTheory.Measure.pi_prod_map_IocProdIoc, measurable_IocProdIoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IicProdIoc_comp_restrict₂ 📖	mathematical	—	Finset.restrict₂ Finset.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset.Iic Finset.Ioc_subset_Iic_self IicProdIoc	—	Finset.Ioc_subset_Iic_self not_le Finset.mem_Ioc
IicProdIoc_def 📖	mathematical	—	IicProdIoc Finset SetLike.instMembership Finset.instSetLike Finset.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE Finset.instMembership Finset.mem_Iic Finset.Ioc Preorder.toLT Finset.mem_Ioc LinearOrder.toPartialOrder not_le	—	—
IicProdIoc_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IicProdIoc Preorder.frestrictLe₂	—	Finset.Iic_subset_Iic LE.le.trans Finset.mem_Iic
IicProdIoc_preimage 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set.preimage IicProdIoc Set.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Set.univ SProd.sprod Set Set.instSProd Preorder.frestrictLe₂ Finset.Ioc Finset.restrict₂ Finset.Ioc_subset_Iic_self	—	Set.ext Finset.Ioc_subset_Iic_self Finset.mem_Iic Finset.mem_Ioc not_le Finset.Iic_subset_Iic LE.le.trans
IicProdIoc_self 📖	mathematical	—	IicProdIoc	—	Finset.mem_Iic
IocProdIoc_preimage 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set.preimage IocProdIoc Set.pi Finset SetLike.instMembership Finset.instSetLike Finset.Ioc Set.univ SProd.sprod Set Set.instSProd Finset.restrict₂ Finset.Ioc_subset_Ioc_right Finset.Ioc_subset_Ioc_left	—	Set.ext Finset.Ioc_subset_Ioc_right Finset.Ioc_subset_Ioc_left LE.le.trans lt_of_le_of_lt not_le
frestrictLe₂_comp_IicProdIoc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.frestrictLe₂ IicProdIoc	—	Finset.Iic_subset_Iic Finset.mem_Iic
measurable_IicProdIoc 📖	mathematical	—	Measurable Prod.instMeasurableSpace MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset.Ioc IicProdIoc	—	measurable_pi_lambda Measurable.eval measurable_fst measurable_snd
measurable_IocProdIoc 📖	mathematical	—	Measurable Prod.instMeasurableSpace MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IocProdIoc	—	measurable_pi_lambda Measurable.eval measurable_fst measurable_snd
restrict₂_comp_IicProdIoc 📖	mathematical	—	Finset.restrict₂ Finset.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset.Iic Finset.Ioc_subset_Iic_self IicProdIoc	—	Finset.Ioc_subset_Iic_self not_le Finset.mem_Ioc

---

← Back to Index