PreorderRestrict

📁 Source: Mathlib/MeasureTheory/MeasurableSpace/PreorderRestrict.lean

Statistics

Metric	Count
Definitions	0
Theorems measurable_frestrictLe, measurable_frestrictLe₂, measurable_restrictLe, measurable_restrictLe₂	4
Total	4

Preorder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_frestrictLe 📖	mathematical	—	Measurable MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic frestrictLe	—	Finset.measurable_restrict
measurable_frestrictLe₂ 📖	mathematical	toLE	Measurable MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic frestrictLe₂	—	Finset.measurable_restrict₂
measurable_restrictLe 📖	mathematical	—	Measurable MeasurableSpace.pi Set.Elem Set.Iic Set Set.instMembership restrictLe	—	Set.measurable_restrict
measurable_restrictLe₂ 📖	mathematical	toLE	Measurable MeasurableSpace.pi Set.Elem Set.Iic Set Set.instMembership restrictLe₂	—	Set.measurable_restrict₂

---

← Back to Index