Restriction

📁 Source: Mathlib/Order/Restriction.lean

Statistics

Metric	Count
Definitions frestrictLe, frestrictLe₂, restrictLe, restrictLe₂	4
Theorems dependsOn_frestrictLe, dependsOn_restrictLe, frestrictLe_apply, frestrictLe_updateFinset, frestrictLe_updateFinset_of_le, frestrictLe₂_apply, frestrictLe₂_comp_frestrictLe, frestrictLe₂_comp_frestrictLe₂, piCongrLeft_comp_frestrictLe, piCongrLeft_comp_restrictLe, restrictLe_apply, restrictLe₂_apply, restrictLe₂_comp_restrictLe, restrictLe₂_comp_restrictLe₂, updateFinset_frestrictLe	15
Total	19

Preorder

Definitions

Name	Category	Theorems
frestrictLe 📖	CompOp	30 math math: ProbabilityTheory.Kernel.condExp_traj', ProbabilityTheory.Kernel.map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure, MeasureTheory.isProjectiveLimit_nat_iff, frestrictLe_iterateInduction, ProbabilityTheory.Kernel.integral_traj_partialTraj', ProbabilityTheory.Kernel.partialTraj_compProd_traj, continuous_frestrictLe, ProbabilityTheory.Kernel.condDistrib_trajMeasure, frestrictLe_updateFinset, ProbabilityTheory.Kernel.condExp_traj, frestrictLe_updateFinset_of_le, frestrictLe₂_comp_frestrictLe, frestrictLe_apply, ProbabilityTheory.Kernel.traj_map_frestrictLe_of_le, ProbabilityTheory.Kernel.integrable_traj, ProbabilityTheory.Kernel.traj_map_frestrictLe, ProbabilityTheory.Kernel.traj_map_frestrictLe_apply, dependsOn_frestrictLe, measurable_frestrictLe, MeasureTheory.Filtration.piLE_eq_comap_frestrictLe, ProbabilityTheory.Kernel.setIntegral_traj_partialTraj, updateFinset_frestrictLe, ProbabilityTheory.Kernel.trajContent_eq_lmarginalPartialTraj, ProbabilityTheory.Kernel.lmarginalPartialTraj_succ, piCongrLeft_comp_restrictLe, ProbabilityTheory.Kernel.lmarginalPartialTraj_eq_lintegral_map, ProbabilityTheory.Kernel.partialTraj_compProd_eq_map_traj, piCongrLeft_comp_frestrictLe, ProbabilityTheory.Kernel.setIntegral_traj_partialTraj', MeasureTheory.isProjectiveLimit_nat_iff'
frestrictLe₂ 📖	CompOp	16 math math: MeasurableEquiv.coe_IicProdIoc_symm, measurable_frestrictLe₂, ProbabilityTheory.Kernel.partialTraj_map_frestrictLe₂_apply, ProbabilityTheory.Kernel.partialTraj_succ_map_frestrictLe₂, ProbabilityTheory.Kernel.partialTraj_le, frestrictLe_updateFinset_of_le, frestrictLe₂_comp_frestrictLe, frestrictLe₂_apply, ProbabilityTheory.Kernel.traj_map_frestrictLe_of_le, IicProdIoc_preimage, ProbabilityTheory.Kernel.partialTraj_map_frestrictLe₂, frestrictLe₂_comp_IicProdIoc, frestrictLe₂_comp_frestrictLe₂, ProbabilityTheory.Kernel.partialTraj_zero, continuous_frestrictLe₂, IicProdIoc_le
restrictLe 📖	CompOp	7 math math: measurable_restrictLe, dependsOn_restrictLe, restrictLe_apply, restrictLe₂_comp_restrictLe, piCongrLeft_comp_restrictLe, piCongrLeft_comp_frestrictLe, continuous_restrictLe
restrictLe₂ 📖	CompOp	5 math math: measurable_restrictLe₂, restrictLe₂_comp_restrictLe₂, restrictLe₂_comp_restrictLe, restrictLe₂_apply, continuous_restrictLe₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dependsOn_frestrictLe 📖	mathematical	—	DependsOn frestrictLe Set.Iic	—	Finset.dependsOn_restrict Finset.coe_Iic
dependsOn_restrictLe 📖	mathematical	—	DependsOn restrictLe Set.Iic	—	Set.dependsOn_restrict
frestrictLe_apply 📖	mathematical	—	frestrictLe Finset SetLike.instMembership Finset.instSetLike Finset.Iic	—	—
frestrictLe_updateFinset 📖	mathematical	—	frestrictLe Function.updateFinset Finset.Iic	—	Function.restrict_updateFinset
frestrictLe_updateFinset_of_le 📖	mathematical	toLE	frestrictLe Function.updateFinset Finset.Iic frestrictLe₂	—	Function.restrict_updateFinset_of_subset Finset.Iic_subset_Iic
frestrictLe₂_apply 📖	mathematical	toLE	frestrictLe₂ Finset SetLike.instMembership Finset.instSetLike Finset.Iic Finset.instHasSubset Finset.Iic_subset_Iic	—	—
frestrictLe₂_comp_frestrictLe 📖	mathematical	toLE	frestrictLe₂ frestrictLe	—	—
frestrictLe₂_comp_frestrictLe₂ 📖	mathematical	toLE	frestrictLe₂ LE.le.trans	—	—
piCongrLeft_comp_frestrictLe 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.piCongrLeft Finset SetLike.instMembership Finset.instSetLike Finset.Iic Set.Elem Set.Iic Set Set.instMembership Equiv.IicFinsetSet frestrictLe restrictLe	—	—
piCongrLeft_comp_restrictLe 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.piCongrLeft Set.Elem Set.Iic Finset SetLike.instMembership Finset.instSetLike Finset.Iic Equiv.symm Equiv.IicFinsetSet restrictLe frestrictLe	—	—
restrictLe_apply 📖	mathematical	—	restrictLe Set Set.instMembership Set.Iic	—	—
restrictLe₂_apply 📖	mathematical	toLE	restrictLe₂ Set Set.instMembership Set.Iic Set.instHasSubset Set.Iic_subset_Iic	—	—
restrictLe₂_comp_restrictLe 📖	mathematical	toLE	restrictLe₂ restrictLe	—	—
restrictLe₂_comp_restrictLe₂ 📖	mathematical	toLE	restrictLe₂ LE.le.trans	—	—
updateFinset_frestrictLe 📖	mathematical	—	Function.updateFinset Finset.Iic frestrictLe	—	Function.updateFinset_restrict

---

← Back to Index