Basic

📁 Source: Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

Statistics

Metric	Count
Definitions `FinStronglyMeasurable`, `approx`, `approx`, `approxBounded`, `«termStronglyMeasurable[_]»`	5
Theorems `comp_stronglyMeasurable`, `stronglyMeasurable`, `stronglyMeasurable_of_hasCompactMulSupport`, `stronglyMeasurable_of_hasCompactSupport`, `stronglyMeasurable_of_mulSupport_subset_isCompact`, `stronglyMeasurable_of_support_subset_isCompact`, `comp_stronglyMeasurable_iff`, `stronglyMeasurable_fun_prod`, `stronglyMeasurable_fun_sum`, `stronglyMeasurable_prod`, `stronglyMeasurable_sum`, `stronglyMeasurable_of_prod`, `stronglyMeasurable_const_smul_iff`, `stronglyMeasurable_fun_prod`, `stronglyMeasurable_fun_sum`, `stronglyMeasurable_prod`, `stronglyMeasurable_sum`, `add_stronglyMeasurable`, `stronglyMeasurable`, `stronglyMeasurable_add`, `sub_stronglyMeasurable`, `exists_stronglyMeasurable_extend`, `stronglyMeasurable_extend`, `add`, `const_smul`, `exists_set_sigmaFinite`, `fin_support_approx`, `inf`, `measurable`, `mul`, `neg`, `stronglyMeasurable`, `sub`, `sup`, `tendsto_approx`, `stronglyMeasurable`, `stronglyMeasurable_prod_apply`, `stronglyMeasurable_sum_apply`, `add`, `add_const`, `add_iff_left`, `add_iff_right`, `ae_eq_trim_iff`, `ae_eq_trim_of_stronglyMeasurable`, `ae_le_trim_iff`, `ae_le_trim_of_stronglyMeasurable`, `aemeasurable`, `comp_fst`, `comp_measurable`, `comp_snd`, `const_add`, `const_mul`, `const_nsmul`, `const_smul`, `const_smul'`, `const_vadd`, `const_vadd'`, `dist`, `div`, `edist`, `enorm`, `exists_spanning_measurableSet_norm_le`, `finStronglyMeasurable`, `finStronglyMeasurable_of_set_sigmaFinite`, `fst`, `indicator`, `induction`, `induction'`, `inf`, `inv`, `isSeparable_range`, `ite`, `measurable`, `measurableSet_eq_fun`, `measurableSet_le`, `measurableSet_lt`, `measurableSet_mulSupport`, `measurableSet_support`, `mono`, `mul`, `mul_const`, `mul_iff_left`, `mul_iff_right`, `neg`, `nnnorm`, `norm`, `norm_approxBounded_le`, `of_discrete`, `of_subsingleton_cod`, `of_subsingleton_dom`, `of_uncurry_left`, `of_uncurry_right`, `piecewise`, `pow`, `prodMk`, `prod_swap`, `real_toNNReal`, `separableSpace_range_union_singleton`, `smul`, `smul_const`, `snd`, `stronglyMeasurable_in_set`, `stronglyMeasurable_of_measurableSpace_le_on`, `sub`, `sup`, `tendsto_approx`, `tendsto_approxBounded_ae`, `tendsto_approxBounded_of_norm_le`, `vadd`, `vadd_const`, `finStronglyMeasurable_iff_measurable`, `finStronglyMeasurable_iff_stronglyMeasurable_and_exists_set_sigmaFinite`, `finStronglyMeasurable_of_measurable`, `finStronglyMeasurable_zero`, `measurable_uncurry_of_continuous_of_measurable`, `stronglyMeasurable_const`, `stronglyMeasurable_const'`, `stronglyMeasurable_one`, `stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable`, `stronglyMeasurable_zero`, `stronglyMeasurable_fun_prod`, `stronglyMeasurable_fun_sum`, `stronglyMeasurable_prod`, `stronglyMeasurable_sum`, `stronglyMeasurable_bot_iff`, `stronglyMeasurable_const_smul_iff`, `stronglyMeasurable_const_smul_iff₀`, `stronglyMeasurable_id`, `stronglyMeasurable_iff_measurable`, `stronglyMeasurable_iff_measurable_separable`, `stronglyMeasurable_of_restrict_of_restrict_compl`, `stronglyMeasurable_of_stronglyMeasurable_union_cover`, `stronglyMeasurable_of_tendsto`	133
Total	138

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_stronglyMeasurable` 📖	—	`Continuous` `MeasureTheory.StronglyMeasurable`	—	—	`Filter.Tendsto.comp` `tendsto` `MeasureTheory.StronglyMeasurable.tendsto_approx`
`stronglyMeasurable` 📖	mathematical	`Continuous`	`MeasureTheory.StronglyMeasurable`	—	`SecondCountableTopologyEither.out` `stronglyMeasurable_iff_measurable_separable` `measurable` `TopologicalSpace.isSeparable_range` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `Measurable.stronglyMeasurable` `BorelSpace.opensMeasurable`
`stronglyMeasurable_of_hasCompactMulSupport` 📖	mathematical	`Continuous` `HasCompactMulSupport`	`MeasureTheory.StronglyMeasurable`	—	`stronglyMeasurable_of_mulSupport_subset_isCompact` `subset_mulTSupport`
`stronglyMeasurable_of_hasCompactSupport` 📖	mathematical	`Continuous` `HasCompactSupport`	`MeasureTheory.StronglyMeasurable`	—	`stronglyMeasurable_of_support_subset_isCompact` `subset_tsupport`
`stronglyMeasurable_of_mulSupport_subset_isCompact` 📖	mathematical	`Continuous` `IsCompact` `Set` `Set.instHasSubset` `Function.mulSupport`	`MeasureTheory.StronglyMeasurable`	—	`stronglyMeasurable_iff_measurable_separable` `measurable` `IsCompact.isSeparable` `isCompact_range_of_mulSupport_subset_isCompact`
`stronglyMeasurable_of_support_subset_isCompact` 📖	mathematical	`Continuous` `IsCompact` `Set` `Set.instHasSubset` `Function.support`	`MeasureTheory.StronglyMeasurable`	—	`stronglyMeasurable_iff_measurable_separable` `measurable` `IsCompact.isSeparable` `isCompact_range_of_support_subset_isCompact`

Embedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_stronglyMeasurable_iff` 📖	mathematical	`Topology.IsEmbedding`	`MeasureTheory.StronglyMeasurable`	—	`stronglyMeasurable_iff_measurable_separable` `Set.mem_range_self` `Topology.IsEmbedding.codRestrict` `Function.Surjective.range_eq` `Set.rangeFactorization_surjective` `isClosed_univ` `MeasureTheory.StronglyMeasurable.measurable` `MeasurableEmbedding.measurable_comp_iff` `Topology.IsClosedEmbedding.measurableEmbedding` `Subtype.borelSpace` `Topology.IsEmbedding.isSeparable_preimage` `MeasureTheory.StronglyMeasurable.isSeparable_range` `Function.Injective.preimage_image` `Topology.IsEmbedding.injective` `Set.range_comp` `Continuous.comp_stronglyMeasurable` `Topology.IsEmbedding.continuous`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stronglyMeasurable_fun_prod` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`prod`	—	`stronglyMeasurable_prod`
`stronglyMeasurable_fun_sum` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`sum`	—	`sum_apply` `stronglyMeasurable_sum`
`stronglyMeasurable_prod` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`prod` `Pi.commMonoid`	—	`prod_induction` `MeasureTheory.StronglyMeasurable.mul` `MeasureTheory.stronglyMeasurable_one`
`stronglyMeasurable_sum` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`sum` `Pi.addCommMonoid`	—	`sum_induction` `MeasureTheory.StronglyMeasurable.add` `MeasureTheory.stronglyMeasurable_zero`

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stronglyMeasurable_of_prod` 📖	mathematical	`Continuous` `instTopologicalSpaceProd` `HasCompactSupport`	`MeasureTheory.StronglyMeasurable` `Prod.instMeasurableSpace`	—	`stronglyMeasurable_iff_measurable_separable` `measurable_of_prod` `IsCompact.isSeparable` `isCompact_range`

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stronglyMeasurable_const_smul_iff` 📖	mathematical	`IsUnit`	`MeasureTheory.StronglyMeasurable` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`stronglyMeasurable_const_smul_iff` `Units.continuousConstSMul`

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stronglyMeasurable_fun_prod` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`stronglyMeasurable_prod`
`stronglyMeasurable_fun_sum` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	—	`Pi.list_sum_apply` `stronglyMeasurable_sum`
`stronglyMeasurable_prod` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Pi.instOne` `MulOne.toOne`	—	`MeasureTheory.stronglyMeasurable_one` `MeasureTheory.StronglyMeasurable.mul`
`stronglyMeasurable_sum` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Pi.instZero` `AddZero.toZero`	—	`MeasureTheory.stronglyMeasurable_zero` `MeasureTheory.StronglyMeasurable.add`

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_stronglyMeasurable` 📖	mathematical	`Measurable` `MeasureTheory.StronglyMeasurable`	`Pi.instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid`	—	`tendsto_pi_nhds` `Filter.Tendsto.add` `tendsto_const_nhds` `measurable_of_tendsto_metrizable` `add_simpleFunc` `ContinuousAdd.measurableAdd`
`stronglyMeasurable` 📖	mathematical	`Measurable`	`MeasureTheory.StronglyMeasurable`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Nontrivial.to_nonempty` `Set.mem_univ` `separableSpace_univ` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `MeasureTheory.SimpleFunc.tendsto_approxOn` `IsClosed.closure_eq`
`stronglyMeasurable_add` 📖	mathematical	`Measurable` `MeasureTheory.StronglyMeasurable`	`Pi.instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid`	—	`tendsto_pi_nhds` `Filter.Tendsto.add` `tendsto_const_nhds` `measurable_of_tendsto_metrizable` `simpleFunc_add` `ContinuousAdd.measurableAdd`
`sub_stronglyMeasurable` 📖	mathematical	`Measurable` `MeasureTheory.StronglyMeasurable`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub_eq_add_neg` `add_stronglyMeasurable` `MeasureTheory.StronglyMeasurable.neg`

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_stronglyMeasurable_extend` 📖	—	`MeasurableEmbedding` `MeasureTheory.StronglyMeasurable`	—	—	`stronglyMeasurable_extend` `MeasureTheory.stronglyMeasurable_const'` `Function.Injective.extend_apply` `injective`
`stronglyMeasurable_extend` 📖	mathematical	`MeasurableEmbedding` `MeasureTheory.StronglyMeasurable`	`Function.extend`	—	`MeasureTheory.SimpleFunc.extend_apply` `Function.Injective.extend_apply` `injective` `MeasureTheory.StronglyMeasurable.tendsto_approx` `MeasureTheory.SimpleFunc.extend_apply'` `Function.extend_apply'`

MeasureTheory

Definitions

Name	Category	Theorems
`FinStronglyMeasurable` 📖	MathDef	11 math math: `StronglyMeasurable.finStronglyMeasurable`, `finStronglyMeasurable_iff_stronglyMeasurable_and_exists_set_sigmaFinite`, `Lp.finStronglyMeasurable`, `ENNReal.finStronglyMeasurable_of_measurable`, `finStronglyMeasurable_zero`, `finStronglyMeasurable_of_measurable`, `finStronglyMeasurable_iff_measurable`, `MemLp.finStronglyMeasurable_of_stronglyMeasurable`, `StronglyMeasurable.finStronglyMeasurable_of_set_sigmaFinite`, `AEFinStronglyMeasurable.finStronglyMeasurable_mk`, `lpMeas.ae_fin_strongly_measurable'`
`«termStronglyMeasurable[_]»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finStronglyMeasurable_iff_measurable` 📖	mathematical	—	`FinStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Measurable`	—	`FinStronglyMeasurable.measurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `StronglyMeasurable.finStronglyMeasurable` `Measurable.stronglyMeasurable` `BorelSpace.opensMeasurable`
`finStronglyMeasurable_iff_stronglyMeasurable_and_exists_set_sigmaFinite` 📖	mathematical	—	`FinStronglyMeasurable` `StronglyMeasurable` `MeasurableSet` `SigmaFinite` `Measure.restrict`	—	`FinStronglyMeasurable.stronglyMeasurable` `FinStronglyMeasurable.exists_set_sigmaFinite` `StronglyMeasurable.finStronglyMeasurable_of_set_sigmaFinite`
`finStronglyMeasurable_of_measurable` 📖	mathematical	`Measurable`	`FinStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`finStronglyMeasurable_iff_measurable`
`finStronglyMeasurable_zero` 📖	mathematical	—	`FinStronglyMeasurable` `Pi.instZero`	—	`Function.support_zero` `measure_empty` `Measure.instOuterMeasureClass` `tendsto_const_nhds`
`measurable_uncurry_of_continuous_of_measurable` 📖	mathematical	`Continuous` `Measurable`	`Prod.instMeasurableSpace`	—	`stronglyMeasurable_id` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `Filter.Tendsto.comp` `Continuous.tendsto` `StronglyMeasurable.tendsto_approx` `tendsto_pi_nhds` `measurable_of_tendsto_metrizable` `measurable_swap_iff` `measurable_from_prod_countable_left` `Finite.to_countable` `Finite.of_fintype` `Subtype.instMeasurableSingletonClass` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `SimpleFunc.mem_range_self` `Measurable.comp` `Measurable.prodMk` `SimpleFunc.measurable` `measurable_fst` `measurable_snd`
`stronglyMeasurable_const` 📖	mathematical	—	`StronglyMeasurable`	—	`tendsto_const_nhds`
`stronglyMeasurable_const'` 📖	mathematical	—	`StronglyMeasurable`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Nontrivial.to_nonempty` `stronglyMeasurable_const`
`stronglyMeasurable_one` 📖	mathematical	—	`StronglyMeasurable` `Pi.instOne`	—	`stronglyMeasurable_const`
`stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable` 📖	mathematical	`Continuous` `StronglyMeasurable`	`Prod.instMeasurableSpace`	—	`stronglyMeasurable_id` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `Filter.Tendsto.comp` `Continuous.tendsto` `StronglyMeasurable.tendsto_approx` `tendsto_pi_nhds` `stronglyMeasurable_of_tendsto` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `stronglyMeasurable_iff_measurable_separable` `measurable_swap_iff` `measurable_from_prod_countable_left` `Finite.to_countable` `Finite.of_fintype` `Subtype.instMeasurableSingletonClass` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `StronglyMeasurable.measurable` `TopologicalSpace.IsSeparable.iUnion` `StronglyMeasurable.isSeparable_range` `TopologicalSpace.IsSeparable.mono` `SimpleFunc.mem_range_self` `StronglyMeasurable.comp_measurable` `Measurable.prodMk` `Measurable.comp` `SimpleFunc.measurable` `measurable_fst` `measurable_snd`
`stronglyMeasurable_zero` 📖	mathematical	—	`StronglyMeasurable` `Pi.instZero`	—	`stronglyMeasurable_const`

MeasureTheory.FinStronglyMeasurable

Definitions

Name	Category	Theorems
`approx` 📖	CompOp	2 math math: `tendsto_approx`, `fin_support_approx`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MeasureTheory.FinStronglyMeasurable` `AddZero.toZero` `AddZeroClass.toAddZero`	`Pi.instAdd` `AddZero.toAdd`	—	`LE.le.trans_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Function.support_add` `MeasureTheory.measure_union_le` `ENNReal.add_lt_top` `fin_support_approx` `Filter.Tendsto.add` `tendsto_approx`
`const_smul` 📖	mathematical	`MeasureTheory.FinStronglyMeasurable`	`Function.hasSMul` `SMulZeroClass.toSMul`	—	`MeasureTheory.SimpleFunc.coe_smul` `LE.le.trans_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Function.support_const_smul_subset` `fin_support_approx` `Filter.Tendsto.const_smul` `ContinuousSMul.continuousConstSMul` `tendsto_approx`
`exists_set_sigmaFinite` 📖	mathematical	`MeasureTheory.FinStronglyMeasurable`	`MeasurableSet` `MeasureTheory.SigmaFinite` `MeasureTheory.Measure.restrict`	—	`MeasureTheory.SimpleFunc.measurableSet_support` `MeasurableSet.iUnion` `instCountableNat` `Set.mem_iUnion` `Set.mem_compl_iff` `tendsto_nhds_unique` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_const_nhds` `MeasureTheory.Measure.restrict_apply'` `Set.union_inter_distrib_right` `Set.compl_inter_self` `Set.empty_union` `LE.le.trans_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.inter_subset_left` `Set.union_iUnion` `Set.compl_union_self`
`fin_support_approx` 📖	mathematical	`MeasureTheory.FinStronglyMeasurable`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Function.support` `MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instFunLike` `approx` `Top.top` `instTopENNReal`	—	—
`inf` 📖	mathematical	`MeasureTheory.FinStronglyMeasurable`	`Pi.instMinForall_mathlib` `SemilatticeInf.toMin`	—	`LE.le.trans_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Function.support_inf` `MeasureTheory.measure_union_lt_top_iff` `fin_support_approx` `Filter.Tendsto.inf_nhds` `tendsto_approx`
`measurable` 📖	mathematical	`MeasureTheory.FinStronglyMeasurable`	`Measurable`	—	`MeasureTheory.StronglyMeasurable.measurable` `stronglyMeasurable`
`mul` 📖	mathematical	`MeasureTheory.FinStronglyMeasurable` `MulZeroClass.toZero`	`Pi.instMul` `MulZeroClass.toMul`	—	`LE.le.trans_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Function.support_mul_subset_left` `fin_support_approx` `Filter.Tendsto.mul` `tendsto_approx`
`neg` 📖	mathematical	`MeasureTheory.FinStronglyMeasurable` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	`Pi.instNeg` `NegZeroClass.toNeg`	—	`Function.support_fun_neg` `fin_support_approx` `Filter.Tendsto.neg` `tendsto_approx`
`stronglyMeasurable` 📖	mathematical	`MeasureTheory.FinStronglyMeasurable`	`MeasureTheory.StronglyMeasurable`	—	`tendsto_approx`
`sub` 📖	mathematical	`MeasureTheory.FinStronglyMeasurable` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	`Pi.instSub` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid`	—	`LE.le.trans_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Function.support_sub` `MeasureTheory.measure_union_le` `ENNReal.add_lt_top` `fin_support_approx` `Filter.Tendsto.sub` `tendsto_approx`
`sup` 📖	mathematical	`MeasureTheory.FinStronglyMeasurable`	`Pi.instMaxForall_mathlib` `SemilatticeSup.toMax`	—	`LE.le.trans_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Function.support_sup` `MeasureTheory.measure_union_lt_top_iff` `fin_support_approx` `Filter.Tendsto.sup_nhds` `tendsto_approx`
`tendsto_approx` 📖	mathematical	`MeasureTheory.FinStronglyMeasurable`	`Filter.Tendsto` `DFunLike.coe` `MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instFunLike` `approx` `Filter.atTop` `Nat.instPreorder` `nhds`	—	—

MeasureTheory.SimpleFunc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stronglyMeasurable` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`tendsto_const_nhds`

MeasureTheory.StronglyMeasurable

Definitions

Name	Category	Theorems
`approx` 📖	CompOp	1 math math: `tendsto_approx`
`approxBounded` 📖	CompOp	3 math math: `tendsto_approxBounded_ae`, `norm_approxBounded_le`, `tendsto_approxBounded_of_norm_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instAdd`	—	`Filter.Tendsto.add` `tendsto_approx`
`add_const` 📖	—	`MeasureTheory.StronglyMeasurable`	—	—	`add` `MeasureTheory.stronglyMeasurable_const`
`add_iff_left` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`add_iff_right` `add_comm`
`add_iff_right` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`add` `IsTopologicalAddGroup.toContinuousAdd` `neg` `IsTopologicalAddGroup.toContinuousNeg` `add_neg_cancel_comm`
`ae_eq_trim_iff` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `MeasureTheory.StronglyMeasurable`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.trim`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_eq_of_ae_eq_trim` `ae_eq_trim_of_stronglyMeasurable`
`ae_eq_trim_of_stronglyMeasurable` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `MeasureTheory.StronglyMeasurable` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`MeasureTheory.Measure.trim`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.eq_1` `MeasureTheory.ae_iff` `MeasureTheory.trim_measurableSet_eq` `MeasurableSet.compl` `measurableSet_eq_fun`
`ae_le_trim_iff` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `MeasureTheory.StronglyMeasurable`	`Filter.EventuallyLE` `Preorder.toLE` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.trim`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_le_of_ae_le_trim` `ae_le_trim_of_stronglyMeasurable`
`ae_le_trim_of_stronglyMeasurable` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `MeasureTheory.StronglyMeasurable` `Filter.EventuallyLE` `Preorder.toLE` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`MeasureTheory.Measure.trim`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyLE.eq_1` `MeasureTheory.ae_iff` `MeasureTheory.trim_measurableSet_eq` `MeasurableSet.compl` `measurableSet_le`
`aemeasurable` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`AEMeasurable`	—	`Measurable.aemeasurable` `measurable`
`comp_fst` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Prod.instMeasurableSpace`	—	`comp_measurable` `measurable_fst`
`comp_measurable` 📖	—	`MeasureTheory.StronglyMeasurable` `Measurable`	—	—	`tendsto_approx`
`comp_snd` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Prod.instMeasurableSpace`	—	`comp_measurable` `measurable_snd`
`const_add` 📖	—	`MeasureTheory.StronglyMeasurable`	—	—	`add` `MeasureTheory.stronglyMeasurable_const`
`const_mul` 📖	—	`MeasureTheory.StronglyMeasurable`	—	—	`mul` `MeasureTheory.stronglyMeasurable_const`
`const_nsmul` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instSMul` `AddMonoid.toNatSMul`	—	`Filter.Tendsto.nsmul` `tendsto_approx`
`const_smul` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Function.hasSMul`	—	`Filter.Tendsto.const_smul` `tendsto_approx`
`const_smul'` 📖	—	`MeasureTheory.StronglyMeasurable`	—	—	`const_smul`
`const_vadd` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`HVAdd.hVAdd` `instHVAdd` `Function.hasVAdd`	—	`Filter.Tendsto.const_vadd` `tendsto_approx`
`const_vadd'` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`HVAdd.hVAdd` `instHVAdd`	—	`const_vadd`
`dist` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`Real` `Real.pseudoMetricSpace` `Dist.dist` `PseudoMetricSpace.toDist`	—	`Continuous.comp_stronglyMeasurable` `continuous_dist` `prodMk`
`div` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instDiv`	—	`Filter.Tendsto.div'` `tendsto_approx`
`edist` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`ENNReal` `ENNReal.instTopologicalSpace` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Continuous.comp_stronglyMeasurable` `continuous_edist` `prodMk`
`enorm` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Measurable` `ENNReal` `ENNReal.measurableSpace` `ENorm.enorm` `ContinuousENorm.toENorm`	—	`measurable` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `ENNReal.instMetrizableSpace` `ENNReal.borelSpace` `Continuous.comp_stronglyMeasurable` `continuous_enorm`
`exists_spanning_measurableSet_norm_le` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`MeasurableSet` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal` `Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instNatCast` `Set.iUnion` `Set.univ`	—	`exists_spanning_measurableSet_le` `measurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `NNReal.borelSpace` `nnnorm` `LE.le.trans_lt` `MeasureTheory.le_trim` `coe_nnnorm` `NNReal.coe_natCast`
`finStronglyMeasurable` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`MeasureTheory.FinStronglyMeasurable`	—	`finStronglyMeasurable_of_set_sigmaFinite` `MeasurableSet.univ` `Set.compl_univ` `instIsEmptyFalse` `MeasureTheory.Measure.restrict_univ`
`finStronglyMeasurable_of_set_sigmaFinite` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `MeasurableSet`	`MeasureTheory.FinStronglyMeasurable`	—	`MeasureTheory.measurableSet_spanningSets` `MeasureTheory.SimpleFunc.restrict_apply` `MeasurableSet.inter` `Set.indicator_of_notMem` `MeasureTheory.SimpleFunc.support_eq` `Set.iUnion_congr_Prop` `MeasureTheory.measure_biUnion_lt_top` `Finset.finite_toSet` `MeasureTheory.SimpleFunc.restrict_preimage_singleton` `Finset.mem_filter` `Finset.mem_coe` `LE.le.trans_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.inter_subset_left` `MeasureTheory.measure_spanningSets_lt_top` `MeasureTheory.Measure.restrict_apply'` `tendsto_approx` `Set.mem_iUnion` `MeasureTheory.iUnion_spanningSets` `MeasureTheory.monotone_spanningSets` `Set.mem_inter` `Set.indicator_of_mem` `Filter.tendsto_atTop'` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `LE.le.trans` `le_max_left` `GE.ge.le` `le_max_right` `tendsto_const_nhds`
`fst` 📖	—	`MeasureTheory.StronglyMeasurable` `instTopologicalSpaceProd`	—	—	`Continuous.comp_stronglyMeasurable` `continuous_fst`
`indicator` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `MeasurableSet`	`Set.indicator`	—	`piecewise` `MeasureTheory.stronglyMeasurable_const`
`induction` 📖	—	`Set.indicator` `AddZero.toZero` `AddZeroClass.toAddZero` `indicator` `MeasureTheory.stronglyMeasurable_const` `Pi.instAdd` `AddZero.toAdd` `MeasureTheory.StronglyMeasurable`	—	—	`indicator` `MeasureTheory.stronglyMeasurable_const` `MeasureTheory.SimpleFunc.stronglyMeasurable` `MeasureTheory.SimpleFunc.induction` `tendsto_approx`
`induction'` 📖	—	`MeasureTheory.stronglyMeasurable_const` `Set.piecewise` `Set` `Set.instMembership` `piecewise` `MeasureTheory.StronglyMeasurable`	—	—	`MeasureTheory.stronglyMeasurable_const` `piecewise` `MeasureTheory.SimpleFunc.stronglyMeasurable` `MeasureTheory.SimpleFunc.induction'` `tendsto_approx`
`inf` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instMinForall_mathlib`	—	`Filter.Tendsto.inf_nhds` `tendsto_approx`
`inv` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instInv`	—	`Filter.Tendsto.inv` `tendsto_approx`
`isSeparable_range` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`TopologicalSpace.IsSeparable` `Set.range`	—	`TopologicalSpace.IsSeparable.closure` `TopologicalSpace.IsSeparable.iUnion` `instCountableNat` `Set.Finite.isSeparable` `MeasureTheory.SimpleFunc.finite_range` `TopologicalSpace.IsSeparable.mono` `mem_closure_of_tendsto` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_approx` `Filter.univ_mem'` `Set.mem_iUnion_of_mem` `Set.mem_range_self`
`ite` 📖	—	`MeasurableSet` `setOf` `MeasureTheory.StronglyMeasurable`	—	—	`piecewise`
`measurable` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Measurable`	—	`measurable_of_tendsto_metrizable` `MeasureTheory.SimpleFunc.measurable` `tendsto_pi_nhds` `tendsto_approx`
`measurableSet_eq_fun` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`MeasurableSet` `setOf`	—	`measurable` `TopologicalSpace.pseudoMetrizableSpace_prod` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `prodMk` `IsClosed.measurableSet` `BorelSpace.opensMeasurable` `isClosed_diagonal` `TopologicalSpace.t2Space_of_metrizableSpace`
`measurableSet_le` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`MeasurableSet` `setOf` `Preorder.toLE`	—	`measurable` `TopologicalSpace.pseudoMetrizableSpace_prod` `prodMk` `IsClosed.measurableSet` `BorelSpace.opensMeasurable` `isClosed_le_prod`
`measurableSet_lt` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`MeasurableSet` `setOf` `Preorder.toLT`	—	`MeasurableSet.inter` `measurableSet_le` `MeasurableSet.compl`
`measurableSet_mulSupport` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`MeasurableSet` `Function.mulSupport`	—	`measurableSet_mulSupport` `OpensMeasurableSpace.toMeasurableSingletonClass` `BorelSpace.opensMeasurable` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `measurable` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace`
`measurableSet_support` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`MeasurableSet` `Function.support`	—	`measurableSet_support` `OpensMeasurableSpace.toMeasurableSingletonClass` `BorelSpace.opensMeasurable` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `measurable` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace`
`mono` 📖	—	`MeasureTheory.StronglyMeasurable` `MeasurableSpace` `MeasurableSpace.instLE`	—	—	`MeasureTheory.SimpleFunc.measurableSet_fiber'` `MeasureTheory.SimpleFunc.finite_range` `tendsto_approx`
`mul` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instMul`	—	`Filter.Tendsto.mul` `tendsto_approx`
`mul_const` 📖	—	`MeasureTheory.StronglyMeasurable`	—	—	`mul` `MeasureTheory.stronglyMeasurable_const`
`mul_iff_left` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`mul_iff_right` `mul_comm`
`mul_iff_right` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`mul` `IsTopologicalGroup.toContinuousMul` `inv` `IsTopologicalGroup.toContinuousInv` `mul_inv_cancel_comm`
`neg` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instNeg`	—	`Filter.Tendsto.neg` `tendsto_approx`
`nnnorm` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`NNReal` `NNReal.instTopologicalSpace` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`Continuous.comp_stronglyMeasurable` `continuous_nnnorm`
`norm` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Real` `Real.pseudoMetricSpace` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`Continuous.comp_stronglyMeasurable` `continuous_norm`
`norm_approxBounded_le` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `Real.instLE` `Real.instZero`	`Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instFunLike` `approxBounded` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField`	—	`LE.le.trans` `norm_smul_le` `NormedSpace.toIsBoundedSMul` `div_zero` `min_eq_right` `Real.instZeroLEOneClass` `norm_zero` `MulZeroClass.mul_zero` `le_total` `min_eq_left` `one_le_div` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `lt_of_le_of_ne` `norm_nonneg` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `one_mul` `div_le_one` `norm_div` `norm_norm` `mul_comm` `mul_div` `div_eq_mul_inv` `mul_assoc` `inv_mul_cancel₀` `Real.norm_of_nonneg` `le_refl`
`of_discrete` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `exists_surjective_nat` `Nontrivial.to_nonempty` `Function.Surjective.forall` `tendsto_nhds_of_eventually_eq`
`of_subsingleton_cod` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable`	—	`Set.Subsingleton.finite` `Set.subsingleton_of_subsingleton` `tendsto_const_nhds`
`of_subsingleton_dom` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable`	—	`Finite.of_subsingleton` `Subsingleton.measurableSingletonClass` `tendsto_const_nhds`
`of_uncurry_left` 📖	—	`MeasureTheory.StronglyMeasurable` `Prod.instMeasurableSpace`	—	—	`comp_measurable` `measurable_prodMk_left`
`of_uncurry_right` 📖	—	`MeasureTheory.StronglyMeasurable` `Prod.instMeasurableSpace`	—	—	`comp_measurable` `measurable_prodMk_right`
`piecewise` 📖	mathematical	`MeasurableSet` `MeasureTheory.StronglyMeasurable`	`Set.piecewise`	—	`Set.piecewise_eq_of_mem` `tendsto_approx` `Set.piecewise_eq_of_notMem`
`pow` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instPow` `Monoid.toNatPow`	—	`Filter.Tendsto.pow` `tendsto_approx`
`prodMk` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`instTopologicalSpaceProd`	—	`nhds_prod_eq` `Filter.Tendsto.prodMk` `tendsto_approx`
`prod_swap` 📖	—	`MeasureTheory.StronglyMeasurable` `Prod.instMeasurableSpace`	—	—	`comp_measurable` `measurable_swap`
`real_toNNReal` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`NNReal` `NNReal.instTopologicalSpace` `Real.toNNReal`	—	`Continuous.comp_stronglyMeasurable` `continuous_real_toNNReal`
`separableSpace_range_union_singleton` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`TopologicalSpace.SeparableSpace` `Set.Elem` `Set` `Set.instUnion` `Set.range` `Set.instSingletonSet` `instTopologicalSpaceSubtype` `Set.instMembership`	—	`TopologicalSpace.IsSeparable.separableSpace` `TopologicalSpace.IsSeparable.union` `isSeparable_range` `Set.Finite.isSeparable` `Set.finite_singleton`
`smul` 📖	—	`MeasureTheory.StronglyMeasurable`	—	—	`Continuous.comp_stronglyMeasurable` `ContinuousSMul.continuous_smul` `prodMk`
`smul_const` 📖	—	`MeasureTheory.StronglyMeasurable`	—	—	`Continuous.comp_stronglyMeasurable` `ContinuousSMul.continuous_smul` `prodMk` `MeasureTheory.stronglyMeasurable_const`
`snd` 📖	—	`MeasureTheory.StronglyMeasurable` `instTopologicalSpaceProd`	—	—	`Continuous.comp_stronglyMeasurable` `continuous_snd`
`stronglyMeasurable_in_set` 📖	mathematical	`MeasurableSet` `MeasureTheory.StronglyMeasurable`	`Filter.Tendsto` `DFunLike.coe` `MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instFunLike` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`MeasureTheory.SimpleFunc.coe_restrict` `Set.indicator_of_mem` `Set.indicator_of_notMem` `tendsto_approx` `tendsto_const_nhds`
`stronglyMeasurable_of_measurableSpace_le_on` 📖	—	`MeasurableSet` `Set` `Set.instInter` `MeasureTheory.StronglyMeasurable`	—	—	`Set.inter_univ` `stronglyMeasurable_in_set` `Set.union_compl_self` `Set.inter_union_distrib_left` `Set.inter_comm` `MeasurableSet.union` `MeasurableSet.inter` `MeasureTheory.SimpleFunc.measurableSet_fiber` `Set.ext` `Set.mem_inter_iff` `Set.mem_preimage` `Set.mem_singleton_iff` `MeasurableSet.compl` `Function.mtr` `MeasurableSet.empty` `MeasureTheory.SimpleFunc.finite_range`
`sub` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instSub`	—	`Filter.Tendsto.sub` `tendsto_approx`
`sup` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Pi.instMaxForall_mathlib`	—	`Filter.Tendsto.sup_nhds` `tendsto_approx`
`tendsto_approx` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`Filter.Tendsto` `DFunLike.coe` `MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instFunLike` `approx` `Filter.atTop` `Nat.instPreorder` `nhds`	—	—
`tendsto_approxBounded_ae` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.Eventually` `Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`Filter.Tendsto` `DFunLike.coe` `MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instFunLike` `approxBounded` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.mp_mem` `Filter.univ_mem'` `tendsto_approxBounded_of_norm_le`
`tendsto_approxBounded_of_norm_le` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm`	`Filter.Tendsto` `DFunLike.coe` `MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instFunLike` `approxBounded` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`tendsto_approx` `norm_eq_zero` `norm_zero` `Filter.Tendsto.norm` `squeeze_zero_norm` `norm_smul` `NormedSpace.toNormSMulClass` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `Real.norm_of_nonneg` `le_min` `zero_le_one` `Real.instZeroLEOneClass` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `LE.le.trans` `norm_nonneg` `min_le_left` `one_mul` `one_smul` `Filter.Tendsto.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `min_eq_left_iff` `one_le_div` `lt_of_le_of_ne` `Filter.Tendsto.min` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `tendsto_const_nhds` `Filter.Tendsto.div` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal`
`vadd` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`HVAdd.hVAdd` `instHVAdd`	—	`Continuous.comp_stronglyMeasurable` `ContinuousVAdd.continuous_vadd` `prodMk`
`vadd_const` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`HVAdd.hVAdd` `instHVAdd`	—	`Continuous.comp_stronglyMeasurable` `ContinuousVAdd.continuous_vadd` `prodMk` `MeasureTheory.stronglyMeasurable_const`

MeasureTheory.StronglyMeasurable.Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stronglyMeasurable_prod_apply` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `Prod.instMeasurableSpace` `Function.HasUncurry.uncurry` `Function.hasUncurryInduction` `Function.hasUncurryBase` `Measurable`	`Finset.prod` `Pi.commMonoid`	—	`Finset.prod_apply` `Finset.stronglyMeasurable_fun_prod` `MeasureTheory.StronglyMeasurable.comp_measurable` `Measurable.prodMk` `measurable_id'`
`stronglyMeasurable_sum_apply` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `Prod.instMeasurableSpace` `Function.HasUncurry.uncurry` `Function.hasUncurryInduction` `Function.hasUncurryBase` `Measurable`	`Finset.sum` `Pi.addCommMonoid`	—	`Finset.sum_apply` `Finset.stronglyMeasurable_fun_sum` `MeasureTheory.StronglyMeasurable.comp_measurable` `Measurable.prodMk` `measurable_id'`

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stronglyMeasurable_fun_prod` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`prod` `map`	—	`stronglyMeasurable_prod`
`stronglyMeasurable_fun_sum` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`sum` `map`	—	`Pi.multiset_sum_apply` `stronglyMeasurable_sum`
`stronglyMeasurable_prod` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`prod` `Pi.commMonoid`	—	`List.stronglyMeasurable_prod`
`stronglyMeasurable_sum` 📖	mathematical	`MeasureTheory.StronglyMeasurable`	`sum` `Pi.addCommMonoid`	—	`List.stronglyMeasurable_sum` `mem_coe`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stronglyMeasurable_bot_iff` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable` `Bot.bot` `MeasurableSpace` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `MeasurableSpace.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`isEmpty_or_nonempty` `IsEmpty.instSubsingleton` `Unique.instSubsingleton` `MeasureTheory.StronglyMeasurable.tendsto_approx` `MeasureTheory.SimpleFunc.simpleFunc_bot` `tendsto_nhds_unique` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `MeasureTheory.stronglyMeasurable_const`
`stronglyMeasurable_const_smul_iff` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`inv_smul_smul` `MeasureTheory.StronglyMeasurable.const_smul'` `MeasureTheory.StronglyMeasurable.const_smul`
`stronglyMeasurable_const_smul_iff₀` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`IsUnit.stronglyMeasurable_const_smul_iff`
`stronglyMeasurable_id` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable`	—	`Measurable.stronglyMeasurable` `measurable_id`
`stronglyMeasurable_iff_measurable` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable` `Measurable`	—	`MeasureTheory.StronglyMeasurable.measurable` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `Measurable.stronglyMeasurable` `BorelSpace.opensMeasurable`
`stronglyMeasurable_iff_measurable_separable` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable` `Measurable` `TopologicalSpace.IsSeparable` `Set.range`	—	`MeasureTheory.StronglyMeasurable.measurable` `MeasureTheory.StronglyMeasurable.isSeparable_range` `TopologicalSpace.IsSeparable.secondCountableTopology` `Measurable.stronglyMeasurable` `Set.mem_range_self` `TopologicalSpace.PseudoMetrizableSpace.subtype` `Subtype.opensMeasurableSpace` `BorelSpace.opensMeasurable` `Continuous.comp_stronglyMeasurable` `continuous_subtype_val`
`stronglyMeasurable_of_restrict_of_restrict_compl` 📖	—	`MeasurableSet` `MeasureTheory.StronglyMeasurable` `Set.Elem` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `Set.restrict` `Compl.compl` `Set.instCompl`	—	—	`stronglyMeasurable_of_stronglyMeasurable_union_cover` `MeasurableSet.compl` `Eq.ge` `Set.union_compl_self`
`stronglyMeasurable_of_stronglyMeasurable_union_cover` 📖	—	`MeasurableSet` `Set` `Set.instHasSubset` `Set.univ` `Set.instUnion` `MeasureTheory.StronglyMeasurable` `Set.Elem` `Subtype.instMeasurableSpace` `Set.instMembership`	—	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Nontrivial.to_nonempty` `CanLift.prf` `Subtype.canLift` `Function.Injective.extend_apply` `Function.extend_apply'` `Subtype.coe_injective` `MeasurableEmbedding.stronglyMeasurable_extend` `MeasurableEmbedding.subtype_coe` `MeasureTheory.stronglyMeasurable_const`
`stronglyMeasurable_of_tendsto` 📖	—	`MeasureTheory.StronglyMeasurable` `Filter.Tendsto` `nhds` `Pi.topologicalSpace`	—	—	`stronglyMeasurable_iff_measurable_separable` `measurable_of_tendsto_metrizable'` `MeasureTheory.StronglyMeasurable.measurable` `Filter.exists_seq_tendsto` `TopologicalSpace.IsSeparable.closure` `TopologicalSpace.IsSeparable.iUnion` `instCountableNat` `MeasureTheory.StronglyMeasurable.isSeparable_range` `TopologicalSpace.IsSeparable.mono` `mem_closure_of_tendsto` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.comp` `tendsto_pi_nhds` `Filter.univ_mem'` `Set.mem_iUnion_of_mem` `Set.mem_range_self`

---

← Back to Index