MeasurablyGenerated

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

Statistics

Metric	Count
Definitions `IsMeasurablyGenerated`, `instBooleanAlgebra`, `instBot`, `instCompl`, `instEmptyCollection`, `instHImp`, `instInf`, `instInsert`, `instInter`, `instMembership`, `instSDiff`, `instSingleton`, `instSup`, `instTop`, `instUnion`	15
Theorems `exists_measurable_mem`, `exists_measurable_mem_of_smallSets`, `exists_measurable_subset`, `iInf_isMeasurablyGenerated`, `inf_isMeasurablyGenerated`, `isMeasurablyGenerated_bot`, `isMeasurablyGenerated_top`, `principal_isMeasurablyGenerated_iff`, `instLawfulSingleton`, `coe_bot`, `coe_compl`, `coe_empty`, `coe_himp`, `coe_insert`, `coe_inter`, `coe_sdiff`, `coe_singleton`, `coe_top`, `coe_union`, `iInter_of_antitone`, `iInter_of_antitone_of_frequently`, `iUnion_of_monotone`, `iUnion_of_monotone_of_frequently`, `inf_eq_inter`, `measurableSet_bliminf`, `measurableSet_blimsup`, `measurableSet_liminf`, `measurableSet_limsup`, `mem_coe`, `principal_isMeasurablyGenerated`, `subtype_bot_eq`, `sup_eq_union`, `generateFrom_singleton`, `generateFrom_singleton_le`, `measurableSet_generateFrom_singleton_iff`, `measurableSet_tendsto`	36
Total	51

Filter

Definitions

Name	Category	Theorems
`IsMeasurablyGenerated` 📖	CompData	19 math math: `nhdsWithin_Ici_isMeasurablyGenerated`, `atBot_isMeasurablyGenerated`, `nhdsWithin_Ioi_isMeasurablyGenerated`, `MeasureTheory.Measure.cofinite.instIsMeasurablyGenerated`, `inf_isMeasurablyGenerated`, `nhdsWithin_uIcc_isMeasurablyGenerated`, `instIsMeasurablyGeneratedCocompactOfR1Space`, `MeasureTheory.ae_isMeasurablyGenerated`, `nhdsWithin_Iic_isMeasurablyGenerated`, `principal_isMeasurablyGenerated_iff`, `isMeasurablyGenerated_top`, `intervalIntegral.FTCFilter.meas_gen`, `nhdsWithin_Iio_isMeasurablyGenerated`, `isMeasurablyGenerated_bot`, `MeasurableSet.nhdsWithin_isMeasurablyGenerated`, `MeasurableSet.principal_isMeasurablyGenerated`, `nhds_isMeasurablyGenerated`, `nhdsWithin_Icc_isMeasurablyGenerated`, `atTop_isMeasurablyGenerated`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iInf_isMeasurablyGenerated` 📖	mathematical	`IsMeasurablyGenerated`	`iInf` `Filter` `instInfSet`	—	`mem_iInf` `Function.Surjective.iInf_comp` `Equiv.surjective` `MeasurableSet.iInter` `Encodable.countable` `Set.Finite.countable` `Set.iInter_mono` `IsMeasurablyGenerated.exists_measurable_subset`
`inf_isMeasurablyGenerated` 📖	mathematical	—	`IsMeasurablyGenerated` `Filter` `instInf`	—	`IsMeasurablyGenerated.exists_measurable_subset` `inter_mem_inf` `MeasurableSet.inter` `Set.inter_subset_inter`
`isMeasurablyGenerated_bot` 📖	mathematical	—	`IsMeasurablyGenerated` `Bot.bot` `Filter` `instBot`	—	`mem_bot` `MeasurableSet.empty` `Set.empty_subset`
`isMeasurablyGenerated_top` 📖	mathematical	—	`IsMeasurablyGenerated` `Top.top` `Filter` `instTop`	—	`univ_mem` `MeasurableSet.univ`
`principal_isMeasurablyGenerated_iff` 📖	mathematical	—	`IsMeasurablyGenerated` `principal` `MeasurableSet`	—	`mem_principal_self` `HasSubset.Subset.antisymm` `Set.instAntisymmSubset`

Filter.Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_measurable_mem` 📖	mathematical	`Filter.Eventually`	`Set` `Filter` `Filter.instMembership` `MeasurableSet`	—	`Filter.IsMeasurablyGenerated.exists_measurable_subset`
`exists_measurable_mem_of_smallSets` 📖	mathematical	`Filter.Eventually` `Set` `Filter.smallSets`	`Filter` `Filter.instMembership` `MeasurableSet`	—	`Filter.eventually_smallSets` `Filter.IsMeasurablyGenerated.exists_measurable_subset`

Filter.IsMeasurablyGenerated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_measurable_subset` 📖	mathematical	`Set` `Filter` `Filter.instMembership`	`MeasurableSet` `Set.instHasSubset`	—	—

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_bot` 📖	mathematical	—	`Set` `MeasurableSet` `Bot.bot` `Subtype.instBot` `BooleanAlgebra.toBot` `Set.instBooleanAlgebra`	—	—
`coe_compl` 📖	mathematical	—	`Set` `MeasurableSet` `Compl.compl` `Subtype.instCompl` `Set.instCompl`	—	—
`coe_empty` 📖	mathematical	—	`Set` `MeasurableSet` `Subtype.instEmptyCollection` `Set.instEmptyCollection`	—	—
`coe_himp` 📖	mathematical	—	`Set` `MeasurableSet` `HImp.himp` `Subtype.instHImp` `BooleanAlgebra.toHImp` `Set.instBooleanAlgebra`	—	—
`coe_insert` 📖	mathematical	—	`Set` `MeasurableSet` `Subtype.instInsert` `Set.instInsert`	—	—
`coe_inter` 📖	mathematical	—	`Set` `MeasurableSet` `Subtype.instInter` `Set.instInter`	—	—
`coe_sdiff` 📖	mathematical	—	`Set` `MeasurableSet` `Subtype.instSDiff` `Set.instSDiff`	—	—
`coe_singleton` 📖	mathematical	—	`Set` `MeasurableSet` `Subtype.instSingleton` `Set.instSingletonSet`	—	—
`coe_top` 📖	mathematical	—	`Set` `MeasurableSet` `Top.top` `Subtype.instTop` `BooleanAlgebra.toTop` `Set.instBooleanAlgebra`	—	—
`coe_union` 📖	mathematical	—	`Set` `MeasurableSet` `Subtype.instUnion` `Set.instUnion`	—	—
`iInter_of_antitone` 📖	mathematical	`Antitone` `Set` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `MeasurableSet`	`Set.iInter`	—	`compl_iff` `Set.compl_iInter` `iUnion_of_monotone` `Antitone.comp` `compl_anti` `compl`
`iInter_of_antitone_of_frequently` 📖	mathematical	`Antitone` `Set` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Filter.Frequently` `MeasurableSet` `Filter.atTop`	`Set.iInter`	—	`compl_iff` `Set.compl_iInter` `iUnion_of_monotone_of_frequently` `Antitone.comp` `compl_anti` `Filter.Frequently.mono` `compl`
`iUnion_of_monotone` 📖	mathematical	`Monotone` `Set` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `MeasurableSet`	`Set.iUnion`	—	`isEmpty_or_nonempty` `Set.iUnion_of_empty` `iUnion_of_monotone_of_frequently` `Filter.Frequently.of_forall` `Filter.atTop_neBot`
`iUnion_of_monotone_of_frequently` 📖	mathematical	`Monotone` `Set` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Filter.Frequently` `MeasurableSet` `Filter.atTop`	`Set.iUnion`	—	`Filter.exists_seq_forall_of_frequently` `Monotone.iUnion_comp_tendsto_atTop` `Filter.atTop_neBot` `SemilatticeSup.instIsDirectedOrder` `iUnion` `instCountableNat`
`inf_eq_inter` 📖	mathematical	—	`Set` `MeasurableSet` `Subtype.instInf` `Subtype.instInter`	—	—
`measurableSet_bliminf` 📖	mathematical	`MeasurableSet`	`Filter.bliminf` `Set` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Filter.atTop` `Nat.instPreorder`	—	`Filter.bliminf_eq_iSup_biInf_of_nat` `iUnion` `instCountableNat` `iInter` `Prop.countable`
`measurableSet_blimsup` 📖	mathematical	`MeasurableSet`	`Filter.blimsup` `Set` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Filter.atTop` `Nat.instPreorder`	—	`Filter.blimsup_eq_iInf_biSup_of_nat` `iInter` `instCountableNat` `iUnion` `Prop.countable`
`measurableSet_liminf` 📖	mathematical	`MeasurableSet`	`Filter.liminf` `Set` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Filter.atTop` `Nat.instPreorder`	—	`measurableSet_bliminf`
`measurableSet_limsup` 📖	mathematical	`MeasurableSet`	`Filter.limsup` `Set` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Filter.atTop` `Nat.instPreorder`	—	`measurableSet_blimsup`
`mem_coe` 📖	mathematical	—	`Set` `Set.instMembership` `MeasurableSet` `Subtype.instMembership`	—	—
`principal_isMeasurablyGenerated` 📖	mathematical	`MeasurableSet`	`Filter.IsMeasurablyGenerated` `Filter.principal`	—	`Filter.principal_isMeasurablyGenerated_iff`
`subtype_bot_eq` 📖	mathematical	—	`Set` `MeasurableSet` `Set.instEmptyCollection` `empty` `Bot.bot` `Subtype.instBot`	—	`empty`
`sup_eq_union` 📖	mathematical	—	`Set` `MeasurableSet` `Subtype.instSup` `Subtype.instUnion`	—	—

MeasurableSet.Subtype

Definitions

Name	Category	Theorems
`instBooleanAlgebra` 📖	CompOp	6 math math: `MeasureTheory.preVariation.Finset.sup_measurableSetSubtype_eq_biUnion`, `MeasureTheory.preVariation.sum_le`, `MeasureTheory.preVariation.sum_le_preVariationFun_iUnion'`, `MeasureTheory.preVariation.exists_Finpartition_sum_ge`, `MeasureTheory.preVariation.exists_Finpartition_sum_gt`, `MeasureTheory.preVariation.sum_le_preVariationFun_of_subset`
`instBot` 📖	CompOp	2 math math: `MeasurableSet.subtype_bot_eq`, `MeasurableSet.coe_bot`
`instCompl` 📖	CompOp	1 math math: `MeasurableSet.coe_compl`
`instEmptyCollection` 📖	CompOp	2 math math: `instLawfulSingleton`, `MeasurableSet.coe_empty`
`instHImp` 📖	CompOp	1 math math: `MeasurableSet.coe_himp`
`instInf` 📖	CompOp	1 math math: `MeasurableSet.inf_eq_inter`
`instInsert` 📖	CompOp	2 math math: `instLawfulSingleton`, `MeasurableSet.coe_insert`
`instInter` 📖	CompOp	2 math math: `MeasurableSet.inf_eq_inter`, `MeasurableSet.coe_inter`
`instMembership` 📖	CompOp	1 math math: `MeasurableSet.mem_coe`
`instSDiff` 📖	CompOp	1 math math: `MeasurableSet.coe_sdiff`
`instSingleton` 📖	CompOp	2 math math: `MeasurableSet.coe_singleton`, `instLawfulSingleton`
`instSup` 📖	CompOp	1 math math: `MeasurableSet.sup_eq_union`
`instTop` 📖	CompOp	1 math math: `MeasurableSet.coe_top`
`instUnion` 📖	CompOp	2 math math: `MeasurableSet.coe_union`, `MeasurableSet.sup_eq_union`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLawfulSingleton` 📖	mathematical	—	`Set` `MeasurableSet` `instEmptyCollection` `instInsert` `instSingleton`	—	`Set.instLawfulSingleton`

MeasurableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`generateFrom_singleton` 📖	mathematical	—	`generateFrom` `Set` `Set.instSingletonSet` `comap` `Set.instMembership` `Top.top` `MeasurableSpace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`le_antisymm` `generateFrom_le` `Set.preimage_singleton_true` `MeasurableSet.mem` `Set.mem_singleton`
`generateFrom_singleton_le` 📖	mathematical	`MeasurableSet`	`MeasurableSpace` `instLE` `generateFrom` `Set` `Set.instSingletonSet`	—	`generateFrom_le` `Set.mem_singleton_iff`

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurableSet_generateFrom_singleton_iff` 📖	mathematical	—	`MeasurableSet` `MeasurableSpace.generateFrom` `Set` `Set.instSingletonSet` `Set.instEmptyCollection` `Compl.compl` `Set.instCompl` `Set.univ`	—	`MeasurableSpace.generateFrom_singleton` `Fintype.complete` `Set.preimage_singleton_true` `Set.preimage_singleton_false`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurableSet_tendsto` 📖	mathematical	`Measurable`	`MeasurableSet` `setOf` `Filter.Tendsto`	—	`Filter.exists_antitone_basis` `Filter.HasBasis.exists_antitone_subbasis` `Filter.hasBasis_self` `Filter.IsMeasurablyGenerated.exists_measurable_subset` `Filter.HasBasis.tendsto_iff` `Filter.HasAntitoneBasis.toHasBasis` `Set.setOf_forall` `Set.setOf_exists` `MeasurableSet.iInter` `instCountableNat` `MeasurableSet.iUnion` `MeasurableSet.biInter` `Set.to_countable` `SetCoe.countable` `MeasurableSet.preimage`

---

← Back to Index