Order

📁 Source: Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean

Statistics

Metric	Count
Definitions	0
Theorems `biInf`, `biSup`, `iInf`, `iSup`, `isGLB`, `isLUB`, `max`, `min`, `measurable`, `measurableInf`, `measurableInf₂`, `measurableSup`, `measurableSup₂`, `borel_eq_generateFrom_Icc_mem`, `borel_eq_generateFrom_Icc_mem_aux`, `borel_eq_generateFrom_Ico_mem`, `borel_eq_generateFrom_Ico_mem_aux`, `borel_eq_generateFrom_Ioc_mem`, `borel_eq_generateFrom_Ioc_mem_aux`, `measurableSet`, `measurable`, `biInf`, `biSup`, `iInf`, `iInf_Prop`, `iSup`, `iSup_Prop`, `isGLB`, `isGLB_of_mem`, `isLUB`, `isLUB_of_mem`, `le'`, `liminf`, `liminf'`, `limsup`, `limsup'`, `lt`, `max`, `min`, `sInf`, `sSup`, `of_mem_nhdsGT`, `of_mem_nhdsGT_aux`, `ext_of_Icc`, `ext_of_Icc'`, `ext_of_Ici`, `ext_of_Ico`, `ext_of_Ico'`, `ext_of_Ico_finite`, `ext_of_Iic`, `ext_of_Ioc`, `ext_of_Ioc'`, `ext_of_Ioc_finite`, `measurable`, `measurableSet`, `measurable`, `aemeasurable_restrict_of_antitoneOn`, `aemeasurable_restrict_of_monotoneOn`, `atBot_isMeasurablyGenerated`, `atTop_isMeasurablyGenerated`, `borel_eq_generateFrom_Icc`, `borel_eq_generateFrom_Ici`, `borel_eq_generateFrom_Ico`, `borel_eq_generateFrom_Iic`, `borel_eq_generateFrom_Iio`, `borel_eq_generateFrom_Ioc`, `borel_eq_generateFrom_Ioc_le`, `borel_eq_generateFrom_Ioi`, `generateFrom_Icc_mem_le_borel`, `generateFrom_Ico_mem_le_borel`, `instIsMeasurablyGeneratedCocompactOfR1Space`, `measurableSet_Icc`, `measurableSet_Ici`, `measurableSet_Ico`, `measurableSet_Iic`, `measurableSet_Iio`, `measurableSet_Ioc`, `measurableSet_Ioi`, `measurableSet_Ioo`, `measurableSet_bddAbove_range`, `measurableSet_bddBelow_range`, `measurableSet_le`, `measurableSet_le'`, `measurableSet_lt`, `measurableSet_lt'`, `measurableSet_uIcc`, `measurableSet_uIoc`, `measurable_le`, `measurable_lt`, `measurable_of_Ici`, `measurable_of_Iic`, `measurable_of_Iio`, `measurable_of_Ioi`, `measure_eq_measure_preimage_add_measure_tsum_Ico_zpow`, `nhdsWithin_Icc_isMeasurablyGenerated`, `nhdsWithin_Ici_isMeasurablyGenerated`, `nhdsWithin_Iic_isMeasurablyGenerated`, `nhdsWithin_Iio_isMeasurablyGenerated`, `nhdsWithin_Ioi_isMeasurablyGenerated`, `nhdsWithin_uIcc_isMeasurablyGenerated`, `nullMeasurableSet_Icc`, `nullMeasurableSet_Ici`, `nullMeasurableSet_Ico`, `nullMeasurableSet_Iic`, `nullMeasurableSet_Iio`, `nullMeasurableSet_Ioc`, `nullMeasurableSet_Ioi`, `nullMeasurableSet_Ioo`, `nullMeasurableSet_le`, `nullMeasurableSet_lt`, `nullMeasurableSet_lt'`	111
Total	111

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInf` 📖	mathematical	`AEMeasurable`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set` `Set.instMembership`	—	`biSup` `OrderDual.borelSpace` `instOrderTopologyOrderDual` `instSecondCountableTopologyOrderDual`
`biSup` 📖	mathematical	`AEMeasurable`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set` `Set.instMembership`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Measurable.biSup` `Filter.mp_mem` `MeasureTheory.ae_ball_iff` `Filter.univ_mem'` `iSup_congr`
`iInf` 📖	mathematical	`AEMeasurable`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`iSup` `OrderDual.borelSpace` `instOrderTopologyOrderDual` `instSecondCountableTopologyOrderDual`
`iSup` 📖	mathematical	`AEMeasurable`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Measurable.iSup` `Filter.mp_mem` `MeasureTheory.ae_all_iff` `Filter.univ_mem'`
`isGLB` 📖	—	`AEMeasurable` `Filter.Eventually` `IsGLB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `setOf` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `isLUB` `OrderDual.borelSpace` `instOrderTopologyOrderDual` `instSecondCountableTopologyOrderDual`
`isLUB` 📖	—	`AEMeasurable` `Filter.Eventually` `IsLUB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `setOf` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `isEmpty_or_nonempty` `aemeasurable_const'` `Filter.Eventually.mono` `LE.le.antisymm` `Nontrivial.to_nonempty` `Set.ext` `aeSeq.mk_eq_fun_of_mem_aeSeqSet` `aeSeq.fun_prop_of_mem_aeSeqSet` `IsGreatest.isLUB` `Eq.ge` `Measurable.isLUB` `aeSeq.measurable` `Filter.EventuallyEq.symm` `MeasureTheory.ite_ae_eq_of_measure_compl_zero` `aeSeq.measure_compl_aeSeqSet_eq_zero`
`max` 📖	mathematical	`AEMeasurable`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Measurable.max` `Filter.EventuallyEq.comp₂`
`min` 📖	mathematical	`AEMeasurable`	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Measurable.min` `Filter.EventuallyEq.comp₂`

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurable` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Measurable`	—	`Monotone.measurable` `instOrderTopologyOrderDual`

ContinuousInf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurableInf` 📖	mathematical	—	`MeasurableInf`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `Continuous.inf` `continuous_const` `continuous_id'`
`measurableInf₂` 📖	mathematical	—	`MeasurableInf₂`	—	`Continuous.measurable` `Prod.opensMeasurableSpace` `BorelSpace.opensMeasurable` `secondCountableTopologyEither_of_right` `continuous_inf`

ContinuousSup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurableSup` 📖	mathematical	—	`MeasurableSup`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `Continuous.sup` `continuous_const` `continuous_id'`
`measurableSup₂` 📖	mathematical	—	`MeasurableSup₂`	—	`Continuous.measurable` `Prod.opensMeasurableSpace` `BorelSpace.opensMeasurable` `secondCountableTopologyEither_of_right` `continuous_sup`

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`borel_eq_generateFrom_Icc_mem` 📖	mathematical	`Dense`	`borel` `MeasurableSpace.generateFrom` `setOf` `Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Icc`	—	`borel_eq_generateFrom_Icc_mem_aux` `instNoBotOrderOfNoMinOrder` `instIsEmptyFalse` `Set.Nonempty.ne_empty` `Set.nonempty_Ioo`
`borel_eq_generateFrom_Icc_mem_aux` 📖	mathematical	`Dense` `Set` `Set.instMembership`	`borel` `MeasurableSpace.generateFrom` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Icc`	—	`le_antisymm` `borel_eq_generateFrom_Iio` `MeasurableSpace.generateFrom_le` `Set.forall_mem_range` `exists_countable_dense_subset_bot_top` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.Subtype.secondCountableTopology` `Set.ext` `exists_le'` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `exists_mem_open` `isOpen_Ioo` `LE.le.trans_lt` `LT.lt.le` `MeasurableSet.biUnion` `MeasurableSet.iUnion` `Prop.countable` `Set.mem_singleton` `Mathlib.Tactic.Push.not_forall_eq` `Mathlib.Tactic.Contrapose.contrapose₁` `ne_of_lt` `le_trans` `le_of_lt` `le_refl` `generateFrom_Icc_mem_le_borel`
`borel_eq_generateFrom_Ico_mem` 📖	mathematical	`Dense`	`borel` `MeasurableSpace.generateFrom` `setOf` `Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ico`	—	`borel_eq_generateFrom_Ico_mem_aux` `instNoBotOrderOfNoMinOrder` `instIsEmptyFalse` `Set.Nonempty.ne_empty` `Set.nonempty_Ioo`
`borel_eq_generateFrom_Ico_mem_aux` 📖	mathematical	`Dense` `Set` `Set.instMembership`	`borel` `MeasurableSpace.generateFrom` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ico`	—	`le_antisymm` `borel_eq_generateFrom_Iio` `MeasurableSpace.generateFrom_le` `Set.forall_mem_range` `exists_countable_dense_subset_bot_top` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.Subtype.secondCountableTopology` `Set.ext` `exists_le'` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `exists_mem_open` `isOpen_Ioo` `LE.le.trans_lt` `LT.lt.le` `LT.lt.trans_le` `MeasurableSet.biUnion` `MeasurableSet.iUnion` `Prop.countable` `Set.mem_singleton` `Mathlib.Tactic.Push.not_forall_eq` `Set.iUnion_congr_Prop` `generateFrom_Ico_mem_le_borel`
`borel_eq_generateFrom_Ioc_mem` 📖	mathematical	`Dense`	`borel` `MeasurableSpace.generateFrom` `setOf` `Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioc`	—	`borel_eq_generateFrom_Ioc_mem_aux` `instNoTopOrderOfNoMaxOrder` `instIsEmptyFalse` `Set.Nonempty.ne_empty` `Set.nonempty_Ioo`
`borel_eq_generateFrom_Ioc_mem_aux` 📖	mathematical	`Dense` `Set` `Set.instMembership`	`borel` `MeasurableSpace.generateFrom` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioc`	—	`Set.ext` `Set.Ico_toDual` `Set.Ioc_toDual` `borel_eq_generateFrom_Ico_mem_aux` `instOrderTopologyOrderDual` `instSecondCountableTopologyOrderDual` `orderDual` `Set.Ioo_toDual`

IsPreconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurableSet` 📖	mathematical	`IsPreconnected`	`MeasurableSet`	—	`Set.OrdConnected.measurableSet` `ordConnected`

LowerSemicontinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurable` 📖	mathematical	`LowerSemicontinuous` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Measurable`	—	`measurable_of_Ioi` `IsOpen.measurableSet` `isOpen_preimage`

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInf` 📖	mathematical	`Measurable`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set` `Set.instMembership`	—	`biSup` `OrderDual.borelSpace` `instOrderTopologyOrderDual` `instSecondCountableTopologyOrderDual`
`biSup` 📖	mathematical	`Measurable`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set` `Set.instMembership`	—	`cbiSup_eq_of_forall` `iSup` `Encodable.countable` `cbiSup_eq_of_not_forall` `sup` `ContinuousSup.measurableSup₂` `TopologicalLattice.toContinuousSup` `LinearOrder.topologicalLattice` `OrderTopology.to_orderClosedTopology` `measurable_const`
`iInf` 📖	mathematical	`Measurable`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`iSup` `OrderDual.borelSpace` `instOrderTopologyOrderDual` `instSecondCountableTopologyOrderDual`
`iInf_Prop` 📖	mathematical	`Measurable`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	`ciInf_eq_ite` `measurable_const`
`iSup` 📖	mathematical	`Measurable`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`isEmpty_or_nonempty` `iSup_of_empty'` `measurableSet_bddAbove_range` `measurable_const` `isLUB_of_mem` `isLUB_ciSup` `csSup_of_not_bddAbove`
`iSup_Prop` 📖	mathematical	`Measurable`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	`ciSup_eq_ite` `measurable_const`
`isGLB` 📖	—	`Measurable` `IsGLB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `setOf`	—	—	`isLUB` `OrderDual.borelSpace` `instOrderTopologyOrderDual` `instSecondCountableTopologyOrderDual`
`isGLB_of_mem` 📖	—	`Measurable` `MeasurableSet` `IsGLB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `setOf` `Set.EqOn` `Compl.compl` `Set` `Set.instCompl`	—	—	`isLUB_of_mem` `OrderDual.borelSpace` `instOrderTopologyOrderDual` `instSecondCountableTopologyOrderDual`
`isLUB` 📖	—	`Measurable` `IsLUB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `setOf`	—	—	`BorelSpace.measurable_eq` `borel_eq_generateFrom_Ioi` `measurable_generateFrom` `lt_isLUB_iff` `Set.setOf_exists` `MeasurableSet.iUnion` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `isOpen_lt'`
`isLUB_of_mem` 📖	—	`Measurable` `MeasurableSet` `IsLUB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `setOf` `Set.EqOn` `Compl.compl` `Set` `Set.instCompl`	—	—	`isEmpty_or_nonempty` `Set.eq_empty_or_nonempty` `Set.eqOn_univ` `Set.compl_empty` `le_antisymm` `Set.piecewise_eq_of_mem` `Set.piecewise_eq_of_notMem` `piecewise` `measurable_const` `Set.setOf_eq_eq_singleton'` `isLUB`
`le'` 📖	mathematical	`Measurable`	`Prop.instMeasurableSpace` `Preorder.toLE` `PartialOrder.toPreorder`	—	`fun_comp` `measurable_le` `prodMk`
`liminf` 📖	mathematical	`Measurable`	`Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Filter.atTop` `Nat.instPreorder`	—	`liminf'` `Filter.atTop_countable_basis` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `instCountableNat` `Set.to_countable` `SetCoe.countable`
`liminf'` 📖	mathematical	`Measurable` `Filter.HasCountableBasis` `Set.Countable`	`Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Filter.HasCountableBasis.countable` `isEmpty_or_nonempty` `Filter.HasBasis.liminf_eq_sSup_iUnion_iInter` `Filter.HasCountableBasis.toHasBasis` `Set.iInter_coe_set` `Set.iInter_congr_Prop` `Set.iUnion_of_empty` `Filter.HasBasis.liminf_eq_ite` `Set.countable_coe_iff` `measurableSet_bddBelow_range` `Set.setOf_forall` `MeasurableSet.iInter` `MeasurableSet.compl` `piecewise` `measurable_const` `iSup` `iInf` `exists_surjective_nat` `find` `MeasurableSet.union`
`limsup` 📖	mathematical	`Measurable`	`Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Filter.atTop` `Nat.instPreorder`	—	`limsup'` `Filter.atTop_countable_basis` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `instCountableNat` `Set.to_countable` `SetCoe.countable`
`limsup'` 📖	mathematical	`Measurable` `Filter.HasCountableBasis` `Set.Countable`	`Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`liminf'` `OrderDual.borelSpace` `instOrderTopologyOrderDual` `instSecondCountableTopologyOrderDual`
`lt` 📖	mathematical	`Measurable`	`Prop.instMeasurableSpace` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`fun_comp` `measurable_lt` `prodMk`
`max` 📖	mathematical	`Measurable`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`max_def'` `piecewise` `measurableSet_le`
`min` 📖	mathematical	`Measurable`	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`min_def` `piecewise` `measurableSet_le`
`sInf` 📖	mathematical	`Measurable`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.image`	—	`sSup` `OrderDual.borelSpace` `instOrderTopologyOrderDual` `instSecondCountableTopologyOrderDual`
`sSup` 📖	mathematical	`Measurable`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.image`	—	`Set.image_eq_range` `Set.Countable.to_subtype` `iSup`

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_mem_nhdsGT` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet`	—	`Set.union_diff_cancel` `Set.singleton_subset_iff` `union` `MeasurableSingletonClass.measurableSet_singleton` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `T25Space.t2Space` `T3Space.t25Space` `T4Space.t3Space` `T5Space.toT4Space` `OrderTopology.t5Space` `lt_of_le_of_ne` `of_mem_nhdsGT_aux` `mem_nhdsGT_iff_exists_Ioo_subset'` `ne_of_lt` `LT.lt.trans_le` `Mathlib.Tactic.Push.not_and_eq` `Mathlib.Tactic.Push.not_forall_eq`
`of_mem_nhdsGT_aux` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT`	`MeasurableSet`	—	`mem_nhdsGT_iff_exists_Ioo_subset'` `lt_or_gt_of_ne` `Set.disjoint_left` `mem_interior` `isOpen_Ioo` `OrderTopology.to_orderClosedTopology` `LT.lt.trans` `Set.PairwiseDisjoint.countable_of_Ioo` `Function.sometimes_spec` `Set.union_diff_cancel` `interior_subset` `union` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `isOpen_interior` `Set.Countable.measurableSet` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `T25Space.t2Space` `T3Space.t25Space` `T4Space.t3Space` `T5Space.toT4Space` `OrderTopology.t5Space`

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_of_Icc` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`ext_of_Icc'` `LT.lt.ne` `measure_Icc_lt_top`
`ext_of_Icc'` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`exists_countable_dense_bot_top` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `Set.Countable.biUnion` `Set.countable_iUnion` `Prop.countable` `Set.countable_singleton` `ext_of_generateFrom_of_cover_subset` `BorelSpace.measurable_eq` `borel_eq_generateFrom_Icc` `isPiSystem_Icc` `Set.iUnion_congr_Prop` `Set.sUnion_eq_univ_iff` `Dense.exists_le'` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `Dense.exists_ge'` `instClosedIicTopology` `LE.le.trans`
`ext_of_Ici` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`ext_of_Iic` `instSecondCountableTopologyOrderDual` `instOrderTopologyOrderDual`
`ext_of_Ico` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Set.Ico` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	—	`ext_of_Ico'` `LT.lt.ne` `measure_Ico_lt_top` `ConditionallyCompleteLinearOrder.toCompactIccSpace`
`ext_of_Ico'` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`exists_countable_dense_bot_top` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `Set.Countable.biUnion` `Set.countable_iUnion` `Prop.countable` `Set.countable_singleton` `ext_of_generateFrom_of_cover_subset` `BorelSpace.measurable_eq` `borel_eq_generateFrom_Ico` `isPiSystem_Ico` `Set.iUnion_congr_Prop` `Set.sUnion_eq_univ_iff` `Dense.exists_le'` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `Dense.exists_gt` `instClosedIicTopology` `LE.le.trans_lt`
`ext_of_Ico_finite` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Set.univ` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`MeasureTheory.ext_of_generate_finite` `BorelSpace.measurable_eq` `borel_eq_generateFrom_Ico` `isPiSystem_Ico`
`ext_of_Iic` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`ext_of_Ioc_finite` `exists_countable_dense_bot_top` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `directedOn_iff_directed` `Monotone.directed_le` `SemilatticeSup.instIsDirectedOrder` `Subtype.mono_coe` `MeasureTheory.biSup_measure_Iic` `Dense.exists_ge'` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `iSup_congr_Prop` `Set.Iic_diff_Iic` `MeasureTheory.measure_diff` `Set.Iic_subset_Iic` `LT.lt.le` `nullMeasurableSet_Iic` `BorelSpace.opensMeasurable` `MeasureTheory.measure_ne_top`
`ext_of_Ioc` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Set.Ioc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	—	`ext_of_Ioc'` `LT.lt.ne` `measure_Ioc_lt_top` `ConditionallyCompleteLinearOrder.toCompactIccSpace`
`ext_of_Ioc'` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`ext_of_Ico'` `instSecondCountableTopologyOrderDual` `instOrderTopologyOrderDual` `OrderDual.noMaxOrder` `Set.Ico_toDual`
`ext_of_Ioc_finite` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Set.univ` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`ext_of_Ico_finite` `instSecondCountableTopologyOrderDual` `instOrderTopologyOrderDual` `Set.Ico_toDual`

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurable` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Measurable`	—	`Set.ordConnected_def` `lt_of_lt_of_le` `measurable_of_Ioi` `Set.OrdConnected.measurableSet` `BorelSpace.opensMeasurable`

Set.OrdConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurableSet` 📖	mathematical	—	`MeasurableSet`	—	`isOpen_biUnion` `isOpen_Ioo` `IsOpen.measurableSet` `Set.finite_diff_iUnion_Ioo` `Set.iUnion₂_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.Ioo_subset_Icc_self` `out` `Set.union_diff_cancel` `MeasurableSet.union` `Set.Finite.measurableSet` `OpensMeasurableSpace.toMeasurableSingletonClass` `T2Space.t1Space` `OrderClosedTopology.to_t2Space`

UpperSemicontinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurable` 📖	mathematical	`UpperSemicontinuous` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Measurable`	—	`measurable_of_Iio` `IsOpen.measurableSet` `isOpen_preimage`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aemeasurable_restrict_of_antitoneOn` 📖	mathematical	`MeasurableSet` `AntitoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AEMeasurable` `MeasureTheory.Measure.restrict`	—	`aemeasurable_restrict_of_monotoneOn` `instOrderTopologyOrderDual`
`aemeasurable_restrict_of_monotoneOn` 📖	mathematical	`MeasurableSet` `MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AEMeasurable` `MeasureTheory.Measure.restrict`	—	`aemeasurable_restrict_of_measurable_subtype` `Monotone.measurable` `Subtype.borelSpace` `Subtype.instOrderClosedTopology`
`atBot_isMeasurablyGenerated` 📖	mathematical	—	`Filter.IsMeasurablyGenerated` `Filter.atBot`	—	`Filter.iInf_isMeasurablyGenerated` `MeasurableSet.principal_isMeasurablyGenerated` `measurableSet_Iic`
`atTop_isMeasurablyGenerated` 📖	mathematical	—	`Filter.IsMeasurablyGenerated` `Filter.atTop`	—	`Filter.iInf_isMeasurablyGenerated` `MeasurableSet.principal_isMeasurablyGenerated` `measurableSet_Ici`
`borel_eq_generateFrom_Icc` 📖	mathematical	—	`borel` `MeasurableSpace.generateFrom` `setOf` `Set` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Icc`	—	`Dense.borel_eq_generateFrom_Icc_mem_aux` `dense_univ` `Set.mem_univ`
`borel_eq_generateFrom_Ici` 📖	mathematical	—	`borel` `MeasurableSpace.generateFrom` `Set.range` `Set` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`borel_eq_generateFrom_Iic` `instSecondCountableTopologyOrderDual` `instOrderTopologyOrderDual`
`borel_eq_generateFrom_Ico` 📖	mathematical	—	`borel` `MeasurableSpace.generateFrom` `setOf` `Set` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ico`	—	`Dense.borel_eq_generateFrom_Ico_mem_aux` `dense_univ` `Set.mem_univ`
`borel_eq_generateFrom_Iic` 📖	mathematical	—	`borel` `MeasurableSpace.generateFrom` `Set.range` `Set` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`borel_eq_generateFrom_Ioi` `le_antisymm` `MeasurableSpace.generateFrom_le` `Set.compl_Iic` `MeasurableSet.compl` `MeasurableSpace.measurableSet_generateFrom` `Set.mem_range` `Set.compl_Ioi`
`borel_eq_generateFrom_Iio` 📖	mathematical	—	`borel` `MeasurableSpace.generateFrom` `Set.range` `Set` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`le_antisymm` `borel_eq_generateFrom_of_subbasis` `OrderTopology.topology_eq_generate_intervals` `MeasurableSpace.generateFrom_le` `em` `CovBy.Ioi_eq` `Set.compl_Iio` `MeasurableSet.compl` `TopologicalSpace.isOpen_biUnion_countable` `isOpen_Ioi` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `Set.Subset.antisymm` `Set.Subset.trans` `Set.iUnion_congr_Prop` `Set.iUnion₂_mono` `Set.Ioi_subset_Ici_self` `Set.iUnion₂_subset` `Set.Ici_subset_Ioi` `MeasurableSet.biUnion` `Set.forall_mem_range` `isOpen_Iio` `instClosedIciTopology`
`borel_eq_generateFrom_Ioc` 📖	mathematical	—	`borel` `MeasurableSpace.generateFrom` `setOf` `Set` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioc`	—	`Dense.borel_eq_generateFrom_Ioc_mem_aux` `dense_univ` `Set.mem_univ`
`borel_eq_generateFrom_Ioc_le` 📖	mathematical	—	`borel` `MeasurableSpace.generateFrom` `setOf` `Set` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioc`	—	`le_antisymm` `borel_eq_generateFrom_Ioc` `MeasurableSpace.generateFrom_mono` `MeasurableSpace.generateFrom_le` `measurableSet_Ioc` `BorelSpace.opensMeasurable` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology`
`borel_eq_generateFrom_Ioi` 📖	mathematical	—	`borel` `MeasurableSpace.generateFrom` `Set.range` `Set` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`borel_eq_generateFrom_Iio` `instOrderTopologyOrderDual`
`generateFrom_Icc_mem_le_borel` 📖	mathematical	—	`MeasurableSpace` `MeasurableSpace.instLE` `MeasurableSpace.generateFrom` `setOf` `Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Icc` `borel`	—	`MeasurableSpace.generateFrom_le` `measurableSet_Icc` `BorelSpace.opensMeasurable`
`generateFrom_Ico_mem_le_borel` 📖	mathematical	—	`MeasurableSpace` `MeasurableSpace.instLE` `MeasurableSpace.generateFrom` `setOf` `Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ico` `borel`	—	`MeasurableSpace.generateFrom_le` `measurableSet_Ico` `BorelSpace.opensMeasurable` `instClosedIciTopology`
`instIsMeasurablyGeneratedCocompactOfR1Space` 📖	mathematical	—	`Filter.IsMeasurablyGenerated` `Filter.cocompact`	—	`Filter.mem_cocompact` `IsCompact.compl_mem_cocompact` `IsCompact.closure` `MeasurableSet.compl` `IsClosed.measurableSet` `isClosed_closure` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.compl_subset_compl` `subset_closure`
`measurableSet_Icc` 📖	mathematical	—	`MeasurableSet` `Set.Icc`	—	`IsClosed.measurableSet` `isClosed_Icc`
`measurableSet_Ici` 📖	mathematical	—	`MeasurableSet` `Set.Ici`	—	`IsClosed.measurableSet` `isClosed_Ici`
`measurableSet_Ico` 📖	mathematical	—	`MeasurableSet` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`MeasurableSet.inter` `measurableSet_Ici` `measurableSet_Iio`
`measurableSet_Iic` 📖	mathematical	—	`MeasurableSet` `Set.Iic`	—	`IsClosed.measurableSet` `isClosed_Iic`
`measurableSet_Iio` 📖	mathematical	—	`MeasurableSet` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsOpen.measurableSet` `isOpen_Iio`
`measurableSet_Ioc` 📖	mathematical	—	`MeasurableSet` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`MeasurableSet.inter` `measurableSet_Ioi` `measurableSet_Iic`
`measurableSet_Ioi` 📖	mathematical	—	`MeasurableSet` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsOpen.measurableSet` `isOpen_Ioi`
`measurableSet_Ioo` 📖	mathematical	—	`MeasurableSet` `Set.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsOpen.measurableSet` `isOpen_Ioo`
`measurableSet_bddAbove_range` 📖	mathematical	`Measurable`	`MeasurableSet` `setOf` `BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.range`	—	`isEmpty_or_nonempty` `Set.eq_empty_of_isEmpty` `instIsEmptySubtype` `measurableSet_le` `BorelSpace.opensMeasurable` `OrderTopology.to_orderClosedTopology` `measurable_const` `Set.setOf_forall` `MeasurableSet.iInter` `Filter.exists_seq_tendsto` `instIsCountablyGenerated_atTop` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `Filter.atTop_neBot` `SemilatticeSup.instIsDirectedOrder` `Set.Subset.antisymm` `Filter.Eventually.exists` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.tendsto_atTop` `LE.le.trans` `Set.mem_range_self` `Set.setOf_exists` `MeasurableSet.iUnion` `instCountableNat`
`measurableSet_bddBelow_range` 📖	mathematical	`Measurable`	`MeasurableSet` `setOf` `BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.range`	—	`measurableSet_bddAbove_range` `OrderDual.borelSpace` `instOrderTopologyOrderDual` `instSecondCountableTopologyOrderDual`
`measurableSet_le` 📖	mathematical	`Measurable`	`MeasurableSet` `setOf` `Preorder.toLE` `PartialOrder.toPreorder`	—	`Measurable.prodMk` `measurableSet_le'`
`measurableSet_le'` 📖	mathematical	—	`MeasurableSet` `Prod.instMeasurableSpace` `setOf` `Preorder.toLE` `PartialOrder.toPreorder`	—	`IsClosed.measurableSet` `Prod.opensMeasurableSpace` `secondCountableTopologyEither_of_right` `OrderClosedTopology.isClosed_le'`
`measurableSet_lt` 📖	mathematical	`Measurable`	`MeasurableSet` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Measurable.prodMk` `measurableSet_lt'`
`measurableSet_lt'` 📖	mathematical	—	`MeasurableSet` `Prod.instMeasurableSpace` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsOpen.measurableSet` `Prod.opensMeasurableSpace` `secondCountableTopologyEither_of_right` `isOpen_lt` `continuous_fst` `continuous_snd`
`measurableSet_uIcc` 📖	mathematical	—	`MeasurableSet` `Set.uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`measurableSet_Icc`
`measurableSet_uIoc` 📖	mathematical	—	`MeasurableSet` `Set.uIoc`	—	`measurableSet_Ioc`
`measurable_le` 📖	mathematical	—	`Measurable` `Prod.instMeasurableSpace` `Prop.instMeasurableSpace` `Preorder.toLE` `PartialOrder.toPreorder`	—	`measurableSet_setOf` `measurableSet_le'`
`measurable_lt` 📖	mathematical	—	`Measurable` `Prod.instMeasurableSpace` `Prop.instMeasurableSpace` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`measurableSet_setOf` `measurableSet_lt'`
`measurable_of_Ici` 📖	mathematical	`MeasurableSet` `Set.preimage` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Measurable`	—	`measurable_of_Iio`
`measurable_of_Iic` 📖	mathematical	`MeasurableSet` `Set.preimage` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Measurable`	—	`measurable_of_Ioi`
`measurable_of_Iio` 📖	mathematical	`MeasurableSet` `Set.preimage` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Measurable`	—	`BorelSpace.measurable_eq` `borel_eq_generateFrom_Iio` `measurable_generateFrom`
`measurable_of_Ioi` 📖	mathematical	`MeasurableSet` `Set.preimage` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Measurable`	—	`BorelSpace.measurable_eq` `borel_eq_generateFrom_Ioi` `measurable_generateFrom`
`measure_eq_measure_preimage_add_measure_tsum_Ico_zpow` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace` `MeasurableSet` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Set.instInter` `Set.preimage` `Set.instSingletonSet` `instZeroENNReal` `Top.top` `instTopENNReal` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Set.Ico` `ENNReal.instPartialOrder` `DivInvMonoid.toZPow` `ENNReal.instDivInvMonoid` `ENNReal.ofNNReal` `SummationFilter.unconditional`	—	`MeasureTheory.measure_union` `Disjoint.inter_left'` `Disjoint.inter_right'` `Disjoint.preimage` `Set.disjoint_singleton_left` `Set.self_notMem_Ioi` `MeasurableSet.inter` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `ENNReal.borelSpace` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `Set.inter_union_distrib_left` `Set.preimage_union` `Set.singleton_union` `Set.Ioi_insert` `bot_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `Set.Ici_bot` `Set.preimage_univ` `Set.inter_univ` `Set.disjoint_left` `lt_irrefl` `LT.lt.trans_le` `le_of_eq` `measurableSet_Ioo` `Set.ext` `eq_or_lt_of_le` `le_top` `LT.lt.ne` `MeasureTheory.measure_iUnion` `instCountableInt` `ENNReal.zpow_le_of_le` `ENNReal.one_le_coe_iff` `LT.lt.le` `Disjoint.symm` `Ne.lt_or_gt` `measurableSet_Ico` `instClosedIciTopology` `ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow` `ENNReal.one_lt_coe_iff` `ENNReal.coe_ne_top` `Set.preimage_iUnion` `Set.inter_iUnion` `add_assoc`
`nhdsWithin_Icc_isMeasurablyGenerated` 📖	mathematical	—	`Filter.IsMeasurablyGenerated` `nhdsWithin` `Set.Icc`	—	`Set.Ici_inter_Iic` `nhdsWithin_inter` `Filter.inf_isMeasurablyGenerated` `nhdsWithin_Ici_isMeasurablyGenerated` `instClosedIciTopology` `nhdsWithin_Iic_isMeasurablyGenerated` `instClosedIicTopology`
`nhdsWithin_Ici_isMeasurablyGenerated` 📖	mathematical	—	`Filter.IsMeasurablyGenerated` `nhdsWithin` `Set.Ici`	—	`MeasurableSet.nhdsWithin_isMeasurablyGenerated` `measurableSet_Ici`
`nhdsWithin_Iic_isMeasurablyGenerated` 📖	mathematical	—	`Filter.IsMeasurablyGenerated` `nhdsWithin` `Set.Iic`	—	`MeasurableSet.nhdsWithin_isMeasurablyGenerated` `measurableSet_Iic`
`nhdsWithin_Iio_isMeasurablyGenerated` 📖	mathematical	—	`Filter.IsMeasurablyGenerated` `nhdsWithin` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`MeasurableSet.nhdsWithin_isMeasurablyGenerated` `measurableSet_Iio`
`nhdsWithin_Ioi_isMeasurablyGenerated` 📖	mathematical	—	`Filter.IsMeasurablyGenerated` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`MeasurableSet.nhdsWithin_isMeasurablyGenerated` `measurableSet_Ioi`
`nhdsWithin_uIcc_isMeasurablyGenerated` 📖	mathematical	—	`Filter.IsMeasurablyGenerated` `nhdsWithin` `Set.uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`nhdsWithin_Icc_isMeasurablyGenerated`
`nullMeasurableSet_Icc` 📖	mathematical	—	`MeasureTheory.NullMeasurableSet` `Set.Icc`	—	`MeasurableSet.nullMeasurableSet` `measurableSet_Icc`
`nullMeasurableSet_Ici` 📖	mathematical	—	`MeasureTheory.NullMeasurableSet` `Set.Ici`	—	`MeasurableSet.nullMeasurableSet` `measurableSet_Ici`
`nullMeasurableSet_Ico` 📖	mathematical	—	`MeasureTheory.NullMeasurableSet` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`MeasurableSet.nullMeasurableSet` `measurableSet_Ico`
`nullMeasurableSet_Iic` 📖	mathematical	—	`MeasureTheory.NullMeasurableSet` `Set.Iic`	—	`MeasurableSet.nullMeasurableSet` `measurableSet_Iic`
`nullMeasurableSet_Iio` 📖	mathematical	—	`MeasureTheory.NullMeasurableSet` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`MeasurableSet.nullMeasurableSet` `measurableSet_Iio`
`nullMeasurableSet_Ioc` 📖	mathematical	—	`MeasureTheory.NullMeasurableSet` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`MeasurableSet.nullMeasurableSet` `measurableSet_Ioc`
`nullMeasurableSet_Ioi` 📖	mathematical	—	`MeasureTheory.NullMeasurableSet` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`MeasurableSet.nullMeasurableSet` `measurableSet_Ioi`
`nullMeasurableSet_Ioo` 📖	mathematical	—	`MeasureTheory.NullMeasurableSet` `Set.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`MeasurableSet.nullMeasurableSet` `measurableSet_Ioo`
`nullMeasurableSet_le` 📖	mathematical	`AEMeasurable`	`MeasureTheory.NullMeasurableSet` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`AEMeasurable.nullMeasurable` `AEMeasurable.prodMk` `measurableSet_le'`
`nullMeasurableSet_lt` 📖	mathematical	`AEMeasurable`	`MeasureTheory.NullMeasurableSet` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`AEMeasurable.nullMeasurable` `AEMeasurable.prodMk` `measurableSet_lt'`
`nullMeasurableSet_lt'` 📖	mathematical	—	`MeasureTheory.NullMeasurableSet` `Prod.instMeasurableSpace` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`MeasurableSet.nullMeasurableSet` `measurableSet_lt'`

---

← Back to Index