Induced

📁 Source: Mathlib/MeasureTheory/OuterMeasure/Induced.lean

Statistics

Metric	Count
Definitions `trim`, `extend`, `inducedOuterMeasure`	3
Theorems `exists_measurable_superset_eq_trim`, `exists_measurable_superset_forall_eq_trim`, `exists_measurable_superset_of_trim_eq_zero`, `le_trim`, `le_trim_iff`, `null_of_trim_null`, `restrict_trim`, `trim_add`, `trim_anti_measurableSpace`, `trim_binop`, `trim_congr`, `trim_eq`, `trim_eq_iInf`, `trim_eq_iInf'`, `trim_eq_trim_iff`, `trim_iSup`, `trim_le_trim_iff`, `trim_mono`, `trim_op`, `trim_smul`, `trim_sum_ge`, `trim_sup`, `trim_top`, `trim_trim`, `trim_zero`, `ennreal_smul_extend`, `extend_congr`, `extend_empty`, `extend_eq`, `extend_eq_top`, `extend_iUnion`, `extend_iUnion_le_tsum_nat`, `extend_iUnion_le_tsum_nat'`, `extend_iUnion_nat`, `extend_mono`, `extend_mono'`, `extend_top`, `extend_union`, `inducedOuterMeasure_caratheodory`, `inducedOuterMeasure_eq`, `inducedOuterMeasure_eq'`, `inducedOuterMeasure_eq_extend`, `inducedOuterMeasure_eq_extend'`, `inducedOuterMeasure_eq_iInf`, `inducedOuterMeasure_exists_set`, `inducedOuterMeasure_preimage`, `inducedOuterMeasure_union_of_false_of_nonempty_inter`, `le_extend`, `le_inducedOuterMeasure`, `smul_extend`	50
Total	53

MeasureTheory

Definitions

Name	Category	Theorems
`extend` 📖	CompOp	19 math math: `ennreal_smul_extend`, `extend_iUnion_le_tsum_nat`, `extend_eq_top`, `extend_mono'`, `extend_mono`, `smul_extend`, `le_extend`, `inducedOuterMeasure_eq_extend`, `extend_empty`, `extend_iUnion`, `extend_iUnion_le_tsum_nat'`, `extend_eq`, `measure_eq_extend`, `extend_top`, `extend_congr`, `extend_union`, `extend_iUnion_nat`, `AddContent.extend_eq_extend`, `inducedOuterMeasure_eq_extend'`
`inducedOuterMeasure` 📖	CompOp	17 math math: `inducedOuterMeasure_caratheodory`, `inducedOuterMeasure_eq'`, `AddContent.isCaratheodory_inducedOuterMeasure_of_mem`, `inducedOuterMeasure_preimage`, `le_inducedOuterMeasure`, `inducedOuterMeasure_exists_set`, `toOuterMeasure_eq_inducedOuterMeasure`, `inducedOuterMeasure_eq_iInf`, `AddContent.inducedOuterMeasure_eq`, `inducedOuterMeasure_eq_extend`, `AddContent.isCaratheodory_inducedOuterMeasure`, `inducedOuterMeasure_eq`, `inducedOuterMeasure_union_of_false_of_nonempty_inter`, `measure_eq_inducedOuterMeasure`, `AddContent.measureCaratheodory_eq_inducedOuterMeasure`, `inducedOuterMeasure_eq_extend'`, `AddContent.measureCaratheodory_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ennreal_smul_extend` 📖	mathematical	—	`ENNReal` `Function.hasSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `extend`	—	`iInf_congr_Prop` `iInf_pos` `iInf_neg` `ENNReal.mul_top`
`extend_congr` 📖	mathematical	—	`extend`	—	`iInf_congr_Prop`
`extend_empty` 📖	mathematical	`Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal`	`extend`	—	`extend_eq`
`extend_eq` 📖	mathematical	—	`extend`	—	`iInf_congr_Prop` `iInf_pos`
`extend_eq_top` 📖	mathematical	—	`extend` `Top.top` `ENNReal` `instTopENNReal`	—	`iInf_congr_Prop` `iInf_neg`
`extend_iUnion` 📖	mathematical	`Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal` `Set.iUnion` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional` `Pairwise` `Function.onFun` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`extend`	—	`nonempty_encodable` `Encodable.iUnion_decode₂` `tsum_iUnion_decode₂` `extend_empty` `extend_iUnion_nat` `Encodable.iUnion_decode₂_cases` `Encodable.iUnion_decode₂_disjoint_on`
`extend_iUnion_le_tsum_nat` 📖	mathematical	`Set` `Set.instEmptyCollection` `MeasurableSet.empty` `ENNReal` `instZeroENNReal` `Set.iUnion` `MeasurableSet.iUnion` `instCountableNat` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	`Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `extend` `MeasurableSet`	—	`MeasurableSet.empty` `MeasurableSet.iUnion` `instCountableNat` `extend_iUnion_le_tsum_nat'` `iUnion_disjointed` `MeasurableSet.disjointed` `disjoint_disjointed` `ENNReal.tsum_le_tsum` `extend_eq` `extend_mono` `disjointed_le`
`extend_iUnion_le_tsum_nat'` 📖	mathematical	`Set.iUnion` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	`extend` `Set`	—	`extend_eq` `Mathlib.Tactic.Push.not_forall_eq` `le_trans` `le_iInf` `ENNReal.le_tsum`
`extend_iUnion_nat` 📖	mathematical	`Set.iUnion` `tsum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	`extend` `Set`	—	`extend_eq`
`extend_mono` 📖	mathematical	`Set` `Set.instEmptyCollection` `MeasurableSet.empty` `ENNReal` `instZeroENNReal` `Set.iUnion` `MeasurableSet.iUnion` `instCountableNat` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional` `MeasurableSet` `Set.instHasSubset`	`Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `extend`	—	`MeasurableSet.empty` `MeasurableSet.iUnion` `instCountableNat` `le_iInf` `extend_union` `disjoint_sdiff_self_right` `MeasurableSet.diff` `extend_eq` `le_iff_exists_add` `ENNReal.instCanonicallyOrderedAdd` `Set.union_diff_cancel`
`extend_mono'` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Set` `Set.instHasSubset`	`extend`	—	`le_iInf` `extend_eq`
`extend_top` 📖	mathematical	—	`extend` `Top.top` `ENNReal` `instTopENNReal` `Pi.instTopForall`	—	`iInf_eq_top`
`extend_union` 📖	mathematical	`Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal` `Set.iUnion` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`extend` `Set.instUnion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`Set.union_eq_iUnion` `extend_iUnion` `Bool.countable` `pairwise_disjoint_on_bool` `tsum_fintype` `SummationFilter.instLeAtTopUnconditional` `Finset.sum_insert` `Finset.sum_singleton`
`inducedOuterMeasure_caratheodory` 📖	mathematical	`Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal` `Set.iUnion` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	`MeasurableSet` `OuterMeasure.caratheodory` `inducedOuterMeasure` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `DFunLike.coe` `OuterMeasure` `OuterMeasure.instFunLikeSetENNReal` `Set.instInter` `Set.instSDiff`	—	`OuterMeasure.isCaratheodory_iff_le` `inducedOuterMeasure_eq_iInf` `le_iInf` `le_trans` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `measure_mono` `OuterMeasure.instOuterMeasureClass` `Set.inter_subset_inter` `subset_refl` `Set.instReflSubset` `Set.diff_subset_diff` `LE.le.trans_eq` `inducedOuterMeasure_eq'`
`inducedOuterMeasure_eq` 📖	mathematical	`Set` `Set.instEmptyCollection` `MeasurableSet.empty` `ENNReal` `instZeroENNReal` `Set.iUnion` `MeasurableSet.iUnion` `instCountableNat` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional` `MeasurableSet`	`DFunLike.coe` `OuterMeasure` `OuterMeasure.instFunLikeSetENNReal` `inducedOuterMeasure`	—	`MeasurableSet.empty` `MeasurableSet.iUnion` `instCountableNat` `inducedOuterMeasure_eq_extend` `extend_eq`
`inducedOuterMeasure_eq'` 📖	mathematical	`Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal` `Set.iUnion` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	`DFunLike.coe` `OuterMeasure` `OuterMeasure.instFunLikeSetENNReal` `inducedOuterMeasure`	—	`inducedOuterMeasure_eq_extend'` `extend_eq`
`inducedOuterMeasure_eq_extend` 📖	mathematical	`Set` `Set.instEmptyCollection` `MeasurableSet.empty` `ENNReal` `instZeroENNReal` `Set.iUnion` `MeasurableSet.iUnion` `instCountableNat` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional` `MeasurableSet`	`DFunLike.coe` `OuterMeasure` `OuterMeasure.instFunLikeSetENNReal` `inducedOuterMeasure` `extend`	—	`MeasurableSet.empty` `MeasurableSet.iUnion` `instCountableNat` `OuterMeasure.ofFunction_eq` `extend_empty` `extend_mono` `extend_iUnion_le_tsum_nat`
`inducedOuterMeasure_eq_extend'` 📖	mathematical	`Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal` `Set.iUnion` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	`DFunLike.coe` `OuterMeasure` `OuterMeasure.instFunLikeSetENNReal` `inducedOuterMeasure` `extend`	—	`OuterMeasure.ofFunction_eq` `extend_empty` `extend_mono'` `extend_iUnion_le_tsum_nat'`
`inducedOuterMeasure_eq_iInf` 📖	mathematical	`Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal` `Set.iUnion` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	`DFunLike.coe` `OuterMeasure` `OuterMeasure.instFunLikeSetENNReal` `inducedOuterMeasure` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.instHasSubset`	—	`le_antisymm` `le_imp_le_of_le_of_le` `measure_mono` `OuterMeasure.instOuterMeasureClass` `le_refl` `le_of_eq` `inducedOuterMeasure_eq'` `le_iInf` `le_trans` `iInf_le_of_le` `iInf_le` `extend_iUnion_le_tsum_nat'`
`inducedOuterMeasure_exists_set` 📖	mathematical	`Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal` `Set.iUnion` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	`Set.instHasSubset` `DFunLike.coe` `OuterMeasure` `OuterMeasure.instFunLikeSetENNReal` `inducedOuterMeasure` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`ENNReal.lt_add_right` `inducedOuterMeasure_eq_iInf` `le_trans` `le_of_eq` `inducedOuterMeasure_eq'` `le_of_lt`
`inducedOuterMeasure_preimage` 📖	mathematical	`Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal` `Set.iUnion` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`OuterMeasure` `OuterMeasure.instFunLikeSetENNReal` `inducedOuterMeasure`	—	`inducedOuterMeasure_eq_iInf` `Function.Surjective.iInf_congr` `Function.Injective.preimage_surjective` `Equiv.injective` `iInf_congr_Prop` `Function.Surjective.preimage_subset_preimage_iff` `Equiv.surjective`
`inducedOuterMeasure_union_of_false_of_nonempty_inter` 📖	mathematical	`Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal`	`DFunLike.coe` `OuterMeasure` `OuterMeasure.instFunLikeSetENNReal` `inducedOuterMeasure` `Set.instUnion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`OuterMeasure.ofFunction_union_of_top_of_nonempty_inter` `extend_empty` `iInf_of_empty`
`le_extend` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `extend`	—	`le_refl`
`le_inducedOuterMeasure` 📖	mathematical	`Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal`	`OuterMeasure` `Preorder.toLE` `PartialOrder.toPreorder` `OuterMeasure.instPartialOrder` `inducedOuterMeasure` `ENNReal.instPartialOrder` `DFunLike.coe` `OuterMeasure.instFunLikeSetENNReal`	—	`extend_empty` `OuterMeasure.le_ofFunction` `le_iInf_iff`
`smul_extend` 📖	mathematical	—	`Function.hasSMul` `ENNReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `ENNReal.instAddCommMonoid` `extend`	—	`iInf_congr_Prop` `iInf_pos` `iInf_neg` `ENNReal.smul_top`

MeasureTheory.OuterMeasure

Definitions

Name	Category	Theorems
`trim` 📖	CompOp	33 math math: `restrict_trim`, `trim_top`, `trim_smul`, `trim_sup`, `trim_zero`, `trim_eq_iInf'`, `trim_le_trim_iff`, `trim_trim`, `exists_measurable_superset_forall_eq_trim`, `trim_anti_measurableSpace`, `MeasureTheory.Measure.trimmed`, `trim_sum_ge`, `trim_congr`, `le_trim`, `MeasureTheory.toMeasure_toOuterMeasure`, `MeasureTheory.Measure.map_toOuterMeasure`, `MeasureTheory.toOuterMeasure_trim_eq_trim_toOuterMeasure`, `le_trim_iff`, `MeasureTheory.Measure.mkMetric'_toOuterMeasure`, `mkMetric'.trim_pre`, `trim_mono`, `trim_binop`, `trim_eq`, `trim_op`, `trim_add`, `MeasureTheory.measure_eq_trim`, `trim_eq_trim_iff`, `MeasureTheory.Measure.trim_le`, `exists_measurable_superset_eq_trim`, `trim_eq_iInf`, `trim_mkMetric`, `trim_iSup`, `StieltjesFunction.outer_trim`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_measurable_superset_eq_trim` 📖	mathematical	—	`Set` `Set.instHasSubset` `MeasurableSet` `DFunLike.coe` `MeasureTheory.OuterMeasure` `ENNReal` `instFunLikeSetENNReal` `trim`	—	`trim_eq_iInf` `Set.subset_univ` `MeasurableSet.univ` `ENNReal.lt_add_right` `Set.subset_iInter` `MeasurableSet.iInter` `instCountableNat` `Filter.Tendsto.add` `ENNReal.instContinuousAdd` `tendsto_const_nhds` `ENNReal.tendsto_inv_nat_nhds_zero` `le_antisymm` `ge_of_tendsto'` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `add_zero` `le_trans` `MeasureTheory.measure_mono` `instOuterMeasureClass` `Set.iInter_subset` `LT.lt.le` `iInf_le_of_le` `iInf_le`
`exists_measurable_superset_forall_eq_trim` 📖	mathematical	—	`Set` `Set.instHasSubset` `MeasurableSet` `DFunLike.coe` `MeasureTheory.OuterMeasure` `ENNReal` `instFunLikeSetENNReal` `trim`	—	`Set.subset_iInter` `MeasurableSet.iInter` `le_antisymm` `mono` `Set.iInter_subset` `LE.le.trans_eq` `MeasureTheory.measure_mono` `instOuterMeasureClass` `trim_eq` `exists_measurable_superset_eq_trim`
`exists_measurable_superset_of_trim_eq_zero` 📖	mathematical	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `trim` `instZeroENNReal`	`Set.instHasSubset` `MeasurableSet`	—	`exists_measurable_superset_eq_trim`
`le_trim` 📖	mathematical	—	`MeasureTheory.OuterMeasure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `trim`	—	`le_trim_iff` `le_rfl`
`le_trim_iff` 📖	mathematical	—	`MeasureTheory.OuterMeasure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `trim` `ENNReal` `ENNReal.instPartialOrder` `DFunLike.coe` `Set` `instFunLikeSetENNReal`	—	`MeasureTheory.le_inducedOuterMeasure` `MeasurableSet.empty` `empty`
`null_of_trim_null` 📖	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `trim` `instZeroENNReal`	—	—	`nonpos_iff_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `LE.le.trans_eq` `le_trim`
`restrict_trim` 📖	mathematical	`MeasurableSet`	`trim` `DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.OuterMeasure` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `restrict`	—	`le_antisymm` `IsScalarTower.right` `restrict_apply` `exists_measurable_superset_eq_trim` `LE.le.trans` `MeasureTheory.measure_mono` `instOuterMeasureClass` `Set.inter_subset` `trim_eq` `MeasurableSet.union` `MeasurableSet.compl` `Set.union_inter_distrib_right` `Set.compl_inter_self` `Set.empty_union` `Set.inter_subset_left` `le_trim_iff` `MeasurableSet.inter` `le_refl`
`trim_add` 📖	mathematical	—	`trim` `MeasureTheory.OuterMeasure` `instAdd`	—	`ext` `trim_binop` `add_apply`
`trim_anti_measurableSpace` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE`	`MeasureTheory.OuterMeasure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `trim`	—	`trim_eq` `le_refl`
`trim_binop` 📖	mathematical	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal`	`trim`	—	`exists_measurable_superset_forall_eq_trim` `instCountableFin` `Matrix.cons_val_succ`
`trim_congr` 📖	mathematical	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal`	`trim`	—	`MeasurableSet.empty` `empty` `MeasureTheory.inducedOuterMeasure.congr_simp`
`trim_eq` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `trim`	—	`MeasureTheory.inducedOuterMeasure_eq'` `MeasurableSet.empty` `empty` `MeasurableSet.iUnion` `instCountableNat` `MeasureTheory.measure_iUnion_le` `instOuterMeasureClass` `MeasureTheory.measure_mono`
`trim_eq_iInf` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `trim` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.instHasSubset` `MeasurableSet`	—	`iInf_comm` `MeasureTheory.inducedOuterMeasure_eq_iInf` `MeasurableSet.empty` `empty` `MeasurableSet.iUnion` `instCountableNat` `MeasureTheory.measure_iUnion_le` `instOuterMeasureClass` `MeasureTheory.measure_mono`
`trim_eq_iInf'` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `trim` `iInf` `Set.instHasSubset` `MeasurableSet` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`trim_eq_iInf` `iInf_subtype` `iInf_congr_Prop` `iInf_and`
`trim_eq_trim_iff` 📖	mathematical	—	`trim` `DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal`	—	—
`trim_iSup` 📖	mathematical	—	`trim` `iSup` `MeasureTheory.OuterMeasure` `instSupSet`	—	`iSup_plift_down` `ext` `exists_measurable_superset_forall_eq_trim` `Option.instCountable` `instCountablePLift` `iSup_apply` `iSup_congr`
`trim_le_trim_iff` 📖	mathematical	—	`MeasureTheory.OuterMeasure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `trim` `ENNReal` `ENNReal.instPartialOrder` `DFunLike.coe` `Set` `instFunLikeSetENNReal`	—	`le_trim_iff` `trim_eq`
`trim_mono` 📖	mathematical	—	`Monotone` `MeasureTheory.OuterMeasure` `PartialOrder.toPreorder` `instPartialOrder` `trim`	—	`iInf₂_mono` `ENNReal.tsum_le_tsum` `iInf_mono`
`trim_op` 📖	mathematical	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal`	`trim`	—	`trim_binop`
`trim_smul` 📖	mathematical	—	`trim` `MeasureTheory.OuterMeasure` `instSMul`	—	`ext` `trim_op` `smul_apply`
`trim_sum_ge` 📖	mathematical	—	`MeasureTheory.OuterMeasure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `sum` `trim`	—	`trim_eq_iInf` `iInf_congr_Prop` `ENNReal.tsum_le_tsum` `iInf_le_of_le` `iInf_le`
`trim_sup` 📖	mathematical	—	`trim` `MeasureTheory.OuterMeasure` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`ext` `trim_binop` `sup_apply`
`trim_top` 📖	mathematical	—	`trim` `Top.top` `MeasureTheory.OuterMeasure` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`top_unique` `le_trim`
`trim_trim` 📖	mathematical	—	`trim`	—	`trim_eq_trim_iff` `trim_eq`
`trim_zero` 📖	mathematical	—	`trim` `MeasureTheory.OuterMeasure` `instZero`	—	`ext` `le_antisymm` `LE.le.trans_eq` `MeasureTheory.measure_mono` `instOuterMeasureClass` `Set.subset_univ` `trim_eq` `MeasurableSet.univ` `zero_le` `ENNReal.instCanonicallyOrderedAdd`

---

← Back to Index