Basic

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

Statistics

Metric	Count
Definitions `IsCountablySpanning`, `comap`, `map`	3
Theorems `prod`, `comap_le`, `iSup'`, `indicator`, `ite`, `iterate`, `le_map`, `measurable_of_countable_ne`, `mono`, `of_comap_le`, `of_le_map`, `piecewise`, `sup_of_left`, `sup_of_right`, `preimage`, `comap_bot`, `comap_comp`, `comap_const`, `comap_eq_generateFrom`, `comap_generateFrom`, `comap_iSup`, `comap_id`, `comap_le_iff_le_map`, `comap_map_le`, `comap_mono`, `comap_sup`, `gc_comap_map`, `le_map_comap`, `map_comp`, `map_const`, `map_def`, `map_iInf`, `map_id`, `map_inf`, `map_mono`, `map_top`, `measurableSet_comap`, `monotone_comap`, `monotone_map`, `measurable`, `comap_measurable`, `isCountablySpanning_measurableSet`, `measurableSet_generateFrom_of_mem_supClosure`, `measurableSet_mulSupport`, `measurableSet_preimage`, `measurableSet_support`, `measurable_comap_iff`, `measurable_const'`, `measurable_from_top`, `measurable_generateFrom`, `measurable_id''`, `measurable_iff_comap_le`, `measurable_iff_le_map`, `measurable_indicator_const_iff`, `measurable_intCast`, `measurable_natCast`, `measurable_of_countable`, `measurable_of_empty`, `measurable_of_empty_codomain`, `measurable_of_finite`, `measurable_of_subsingleton_codomain`, `measurable_one`, `measurable_zero`	63
Total	66

IsCountablySpanning

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	`IsCountablySpanning`	`Set.image2` `Set` `SProd.sprod` `Set.instSProd`	—	`Set.mem_image2_of_mem` `Set.iUnion_unpair_prod` `Set.univ_prod_univ`

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_le` 📖	mathematical	`Measurable`	`MeasurableSpace` `MeasurableSpace.instLE` `MeasurableSpace.comap`	—	`measurable_iff_comap_le`
`iSup'` 📖	mathematical	`Measurable`	`iSup` `MeasurableSpace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice`	—	`mono` `le_iSup` `le_rfl`
`indicator` 📖	mathematical	`Measurable` `MeasurableSet`	`Set.indicator`	—	`piecewise` `measurable_const`
`ite` 📖	—	`MeasurableSet` `setOf` `Measurable`	—	—	`piecewise`
`iterate` 📖	mathematical	`Measurable`	`Nat.iterate`	—	`measurable_id` `comp`
`le_map` 📖	mathematical	`Measurable`	`MeasurableSpace` `MeasurableSpace.instLE` `MeasurableSpace.map`	—	`measurable_iff_le_map`
`measurable_of_countable_ne` 📖	—	`Measurable`	—	—	`Set.compl_union_self` `Set.inter_univ` `MeasurableSet.union` `Set.Countable.measurableSet` `Set.Countable.mono` `Set.inter_subset_right` `Set.ext` `MeasurableSet.inter` `MeasurableSet.of_compl`
`mono` 📖	—	`Measurable` `MeasurableSpace` `MeasurableSpace.instLE`	—	—	—
`of_comap_le` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `MeasurableSpace.comap`	`Measurable`	—	`measurable_iff_comap_le`
`of_le_map` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `MeasurableSpace.map`	`Measurable`	—	`measurable_iff_le_map`
`piecewise` 📖	mathematical	`MeasurableSet` `Measurable`	`Set.piecewise`	—	`Set.piecewise_preimage` `MeasurableSet.ite`
`sup_of_left` 📖	mathematical	`Measurable`	`MeasurableSpace` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice`	—	`mono` `le_sup_left` `le_rfl`
`sup_of_right` 📖	mathematical	`Measurable`	`MeasurableSpace` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice`	—	`mono` `le_sup_right` `le_rfl`

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage` 📖	mathematical	`MeasurableSet` `Measurable`	`Set.preimage`	—	—

MeasurableSpace

Definitions

Name	Category	Theorems
`comap` 📖	CompOp	74 math math: `comap_eq_generateFrom`, `ProbabilityTheory.condDistrib_ae_eq_condExp`, `comap_mono`, `comap_const`, `CountablyGenerated.comap`, `comap_bot`, `ProbabilityTheory.condExp_ae_eq_integral_condDistrib_id`, `comap_comp`, `ProbabilityTheory.IndepFun_iff_Indep`, `ProbabilityTheory.condExp_ae_eq_integral_condDistrib`, `ProbabilityTheory.Kernel.iIndepFun.iIndep`, `ProbabilityTheory.stronglyMeasurable_integral_condDistrib`, `ProbabilityTheory.measurable_condDistrib`, `Measurable.comap_le`, `indep_comap_of_bcf`, `comap_compl`, `ProbabilityTheory.iIndepFun.indep_comap_natural_of_lt`, `ProbabilityTheory.aestronglyMeasurable_integral_condDistrib`, `indepSets_comap_of_bcf`, `ProbabilityTheory.condDistrib_apply_ae_eq_condExpKernel_map`, `ProbabilityTheory.iIndep_comap_mem_iff`, `ProbabilityTheory.iIndepFun_iff_iIndep`, `measurableSet_comap`, `indep_comap_pi_of_bcf`, `ProbabilityTheory.iIndepFun.iIndep`, `comap_prodMk`, `comap_id`, `ProbabilityTheory.iIndepSet.iIndep_comap_mem`, `ProbabilityTheory.condIndepFun_self_left`, `measurable_iff_comap_le`, `ProbabilityTheory.Kernel.iIndep_comap_mem_iff`, `ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib`, `indep_comap_process_of_bcf`, `comap_prodMap`, `ProbabilityTheory.condIndepFun_self_right`, `measurable_comap_iff`, `comap_iSup`, `MeasureTheory.map_trim_comap`, `indep_comap_process_of_prod_bcf`, `ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib₀`, `MeasureTheory.Filtration.piFinset_eq_comap_restrict`, `gc_comap_map`, `comap_measurable`, `indepSets_comap_pi_of_bcf`, `indepSets_comap_pi_of_prod_bcf`, `MeasureTheory.integral_condExp_indicator`, `ProbabilityTheory.condExp_ae_eq_integral_condDistrib'`, `comap_sup`, `MeasureTheory.AEStronglyMeasurable.comp_ae_measurable'`, `indepSets_comap_process_of_bcf`, `generateFrom_singleton`, `comap_le_iff_le_map`, `MeasureTheory.comap_eval_le_generateFrom_squareCylinders_singleton`, `MeasureTheory.Filtration.piLE_eq_comap_frestrictLe`, `indep_comap_pi_of_prod_bcf`, `comap_map_le`, `ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight`, `MeasurableEmbedding.iff_comap_eq`, `MeasurableEmbedding.comap_eq`, `indepSets_comap_process_of_prod_bcf`, `ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft`, `le_map_comap`, `comap_le_comap_pi`, `borel_comap`, `comap_generateFrom`, `ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib'`, `ProbabilityTheory.iCondIndepFun_iff_iCondIndep`, `ProbabilityTheory.condIndepFun_iff_condIndep`, `MeasureTheory.ae_map_iff_ae_trim`, `MeasureTheory.trim_comap_apply`, `IndepFun.singleton_indepSets_of_indicator`, `comap_not`, `monotone_comap`, `ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib`
`map` 📖	CompOp	20 math math: `Measurable.map_measurableSpace_eq`, `map_def`, `map_mono`, `map_id`, `map_const`, `map_inf`, `Measurable.le_map`, `Continuous.map_eq_borel`, `Continuous.map_borel_eq`, `gc_comap_map`, `map_iInf`, `comap_le_iff_le_map`, `measurable_iff_le_map`, `comap_map_le`, `map_top`, `le_map_comap`, `MeasurableEquiv.map_eq`, `monotone_map`, `Measurable.map_measurableSpace_eq_borel`, `map_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_bot` 📖	mathematical	—	`comap` `Bot.bot` `MeasurableSpace` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`GaloisConnection.l_bot` `gc_comap_map`
`comap_comp` 📖	mathematical	—	`comap`	—	`ext`
`comap_const` 📖	mathematical	—	`comap` `Bot.bot` `MeasurableSpace` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`eq_bot_iff` `Set.preimage_const_of_mem` `Set.preimage_const_of_notMem`
`comap_eq_generateFrom` 📖	mathematical	—	`comap` `generateFrom` `setOf` `Set` `MeasurableSet` `Set.preimage`	—	`generateFrom_measurableSet`
`comap_generateFrom` 📖	mathematical	—	`comap` `generateFrom` `Set.image` `Set` `Set.preimage`	—	`le_antisymm` `comap_le_iff_le_map` `generateFrom_le` `Set.mem_image_of_mem`
`comap_iSup` 📖	mathematical	—	`comap` `iSup` `MeasurableSpace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `gc_comap_map`
`comap_id` 📖	mathematical	—	`comap`	—	`ext`
`comap_le_iff_le_map` 📖	mathematical	—	`MeasurableSpace` `instLE` `comap` `map`	—	—
`comap_map_le` 📖	mathematical	—	`MeasurableSpace` `instLE` `comap` `map`	—	`GaloisConnection.l_u_le` `gc_comap_map`
`comap_mono` 📖	mathematical	`MeasurableSpace` `instLE`	`comap`	—	`GaloisConnection.monotone_l` `gc_comap_map`
`comap_sup` 📖	mathematical	—	`comap` `MeasurableSpace` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `gc_comap_map`
`gc_comap_map` 📖	mathematical	—	`GaloisConnection` `MeasurableSpace` `PartialOrder.toPreorder` `instPartialOrder` `comap` `map`	—	`comap_le_iff_le_map`
`le_map_comap` 📖	mathematical	—	`MeasurableSpace` `instLE` `map` `comap`	—	`GaloisConnection.le_u_l` `gc_comap_map`
`map_comp` 📖	mathematical	—	`map`	—	`ext`
`map_const` 📖	mathematical	—	`map` `Top.top` `MeasurableSpace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`eq_top_iff` `map_def` `Set.preimage_const_of_mem` `Set.preimage_const_of_notMem`
`map_def` 📖	mathematical	—	`MeasurableSet` `map` `Set.preimage`	—	—
`map_iInf` 📖	mathematical	—	`map` `iInf` `MeasurableSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisConnection.u_iInf` `gc_comap_map`
`map_id` 📖	mathematical	—	`map`	—	`ext`
`map_inf` 📖	mathematical	—	`map` `MeasurableSpace` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisConnection.u_inf` `gc_comap_map`
`map_mono` 📖	mathematical	`MeasurableSpace` `instLE`	`map`	—	`GaloisConnection.monotone_u` `gc_comap_map`
`map_top` 📖	mathematical	—	`map` `Top.top` `MeasurableSpace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`GaloisConnection.u_top` `gc_comap_map`
`measurableSet_comap` 📖	mathematical	—	`MeasurableSet` `comap` `Set.preimage`	—	—
`monotone_comap` 📖	mathematical	—	`Monotone` `MeasurableSpace` `PartialOrder.toPreorder` `instPartialOrder` `comap`	—	`comap_mono`
`monotone_map` 📖	mathematical	—	`Monotone` `MeasurableSpace` `PartialOrder.toPreorder` `instPartialOrder` `map`	—	`map_mono`

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurable` 📖	mathematical	—	`Measurable`	—	`measurableSet`

(root)

Definitions

Name	Category	Theorems
`IsCountablySpanning` 📖	MathDef	3 math math: `isCountablySpanning_measurableSet`, `MeasureTheory.isCountablySpanning_spanningSets`, `MeasureTheory.Measure.FiniteSpanningSetsIn.isCountablySpanning`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_measurable` 📖	mathematical	—	`Measurable` `MeasurableSpace.comap`	—	—
`isCountablySpanning_measurableSet` 📖	mathematical	—	`IsCountablySpanning` `setOf` `Set` `MeasurableSet`	—	`MeasurableSet.univ` `Set.iUnion_const`
`measurableSet_generateFrom_of_mem_supClosure` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `supClosure` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice`	`MeasurableSet` `MeasurableSpace.generateFrom`	—	`Finset.sup'_eq_sup` `Finset.sup_id_set_eq_sUnion` `MeasurableSet.sUnion` `Finset.countable_toSet` `MeasurableSpace.measurableSet_generateFrom`
`measurableSet_mulSupport` 📖	mathematical	`Measurable`	`MeasurableSet` `Function.mulSupport`	—	`MeasurableSet.compl` `MeasurableSingletonClass.measurableSet_singleton`
`measurableSet_preimage` 📖	mathematical	`Measurable` `MeasurableSet`	`Set.preimage`	—	—
`measurableSet_support` 📖	mathematical	`Measurable`	`MeasurableSet` `Function.support`	—	`MeasurableSet.compl` `MeasurableSingletonClass.measurableSet_singleton`
`measurable_comap_iff` 📖	mathematical	—	`Measurable` `MeasurableSpace.comap`	—	`MeasurableSpace.comap_comp`
`measurable_const'` 📖	mathematical	—	`Measurable`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Nontrivial.to_nonempty` `measurable_const`
`measurable_from_top` 📖	mathematical	—	`Measurable` `Top.top` `MeasurableSpace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `MeasurableSpace.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	—
`measurable_generateFrom` 📖	mathematical	`MeasurableSet` `Set.preimage`	`Measurable` `MeasurableSpace.generateFrom`	—	`Measurable.of_le_map` `MeasurableSpace.generateFrom_le`
`measurable_id''` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE`	`Measurable`	—	`Measurable.mono` `measurable_id` `le_rfl`
`measurable_iff_comap_le` 📖	mathematical	—	`Measurable` `MeasurableSpace` `MeasurableSpace.instLE` `MeasurableSpace.comap`	—	`MeasurableSpace.comap_le_iff_le_map`
`measurable_iff_le_map` 📖	mathematical	—	`Measurable` `MeasurableSpace` `MeasurableSpace.instLE` `MeasurableSpace.map`	—	—
`measurable_indicator_const_iff` 📖	mathematical	—	`Measurable` `Set.indicator` `MeasurableSet`	—	`Set.ext` `MeasurableSet.compl` `MeasurableSet.singleton` `Measurable.indicator` `measurable_const`
`measurable_intCast` 📖	mathematical	—	`Measurable` `Pi.instIntCast`	—	`measurable_const`
`measurable_natCast` 📖	mathematical	—	`Measurable` `Pi.instNatCast`	—	`measurable_const`
`measurable_of_countable` 📖	mathematical	—	`Measurable`	—	`Set.Countable.measurableSet` `Set.to_countable` `SetCoe.countable`
`measurable_of_empty` 📖	mathematical	—	`Measurable`	—	`Subsingleton.measurable` `IsEmpty.instSubsingleton`
`measurable_of_empty_codomain` 📖	mathematical	—	`Measurable`	—	`measurable_of_subsingleton_codomain` `IsEmpty.instSubsingleton`
`measurable_of_finite` 📖	mathematical	—	`Measurable`	—	`measurable_of_countable` `Finite.to_countable`
`measurable_of_subsingleton_codomain` 📖	mathematical	—	`Measurable`	—	`Subsingleton.set_cases` `MeasurableSet.empty` `MeasurableSet.univ`
`measurable_one` 📖	mathematical	—	`Measurable` `Pi.instOne`	—	`measurable_const`
`measurable_zero` 📖	mathematical	—	`Measurable` `Pi.instZero`	—	`measurable_const`

---

← Back to Index