Operations

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

Statistics

Metric	Count
Definitions `addCommMonoid`, `coeFnAddMonoidHom`, `comap`, `dirac`, `instAdd`, `instBot`, `instCompleteLattice`, `instDistribMulAction`, `instFunctor`, `instInhabited`, `instModule`, `instMulAction`, `instPartialOrder`, `instSMul`, `instSupSet`, `instZero`, `map`, `orderBot`, `restrict`, `sum`	20
Theorems `add_apply`, `coeFnAddMonoidHom_apply`, `coe_add`, `coe_bot`, `coe_iSup`, `coe_smul`, `coe_zero`, `comap_apply`, `comap_iSup`, `comap_map`, `comap_mono`, `comap_top`, `dirac_apply`, `iSup_apply`, `instIsCentralScalar`, `instIsOrderedAddMonoid`, `instIsScalarTower`, `instLawfulFunctor`, `instSMulCommClass`, `le_comap_map`, `map_apply`, `map_comap`, `map_comap_le`, `map_comap_of_surjective`, `map_iSup`, `map_id`, `map_le_restrict_range`, `map_map`, `map_mono`, `map_sup`, `map_top`, `map_top_of_surjective`, `mono''`, `restrict_apply`, `restrict_empty`, `restrict_iSup`, `restrict_le_self`, `restrict_mono`, `restrict_univ`, `sSup_apply`, `smul_apply`, `smul_dirac_apply`, `smul_iSup`, `sum_apply`, `sup_apply`, `top_apply`, `top_apply'`, `univ_eq_zero_iff`	48
Total	68

MeasureTheory.OuterMeasure

Definitions

Name	Category	Theorems
`addCommMonoid` 📖	CompOp	47 math math: `map_iInf`, `comap_map`, `restrict_trim`, `comap_iInf`, `map_apply`, `restrict_iInf`, `comap_apply`, `restrict_ofFunction`, `map_iInf_comap`, `map_comap_le`, `map_le_restrict_range`, `isometry_comap_mkMetric`, `map_comap`, `restrict_univ`, `map_iInf_le`, `MeasureTheory.Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict`, `comap_top`, `map_map`, `restrict_empty`, `map_ofFunction`, `map_comap_of_surjective`, `map_iSup`, `restrict_iSup`, `comap_mono`, `le_comap_map`, `coeFnAddMonoidHom_apply`, `MeasureTheory.Measure.map_toOuterMeasure`, `isometryEquiv_map_mkMetric`, `restrict_biInf`, `restrict_sInf_eq_sInf_restrict`, `comap_boundedBy`, `map_id`, `isometry_map_mkMetric`, `map_top_of_surjective`, `restrict_apply`, `instIsOrderedAddMonoid`, `map_top`, `restrict_mono`, `comap_iSup`, `map_biInf_comap`, `restrict_iInf_restrict`, `map_ofFunction_le`, `map_sup`, `comap_ofFunction`, `map_mono`, `restrict_le_self`, `isometryEquiv_comap_mkMetric`
`coeFnAddMonoidHom` 📖	CompOp	1 math math: `coeFnAddMonoidHom_apply`
`comap` 📖	CompOp	16 math math: `comap_map`, `comap_iInf`, `comap_apply`, `map_iInf_comap`, `map_comap_le`, `isometry_comap_mkMetric`, `map_comap`, `comap_top`, `map_comap_of_surjective`, `comap_mono`, `le_comap_map`, `comap_boundedBy`, `comap_iSup`, `map_biInf_comap`, `comap_ofFunction`, `isometryEquiv_comap_mkMetric`
`dirac` 📖	CompOp	3 math math: `dirac_apply`, `dirac_caratheodory`, `smul_dirac_apply`
`instAdd` 📖	CompOp	5 math math: `coe_add`, `add_apply`, `le_add_caratheodory`, `trim_add`, `MeasureTheory.Measure.add_toOuterMeasure`
`instBot` 📖	CompOp	1 math math: `coe_bot`
`instCompleteLattice` 📖	CompOp	32 math math: `map_iInf`, `mkMetric_top`, `trim_top`, `comap_iInf`, `iInf_apply'`, `MeasureTheory.Measure.sInf_caratheodory`, `restrict_iInf`, `map_iInf_comap`, `trim_sup`, `map_iInf_le`, `comap_top`, `iInf_apply`, `biInf_apply`, `top_caratheodory`, `sup_apply`, `MeasureTheory.Measure.sInf_apply`, `sInf_apply`, `restrict_biInf`, `boundedBy_top`, `restrict_sInf_eq_sInf_restrict`, `top_apply'`, `MeasureTheory.Measure.toOuterMeasure_top`, `sInf_apply'`, `map_top_of_surjective`, `sInf_eq_boundedBy_sInfGen`, `map_top`, `biInf_apply'`, `top_apply`, `map_biInf_comap`, `restrict_iInf_restrict`, `map_sup`, `toMeasure_top`
`instDistribMulAction` 📖	CompOp	—
`instFunctor` 📖	CompOp	1 math math: `instLawfulFunctor`
`instInhabited` 📖	CompOp	—
`instModule` 📖	CompOp	45 math math: `map_iInf`, `comap_map`, `restrict_trim`, `comap_iInf`, `map_apply`, `restrict_iInf`, `comap_apply`, `restrict_ofFunction`, `map_iInf_comap`, `map_comap_le`, `map_le_restrict_range`, `isometry_comap_mkMetric`, `map_comap`, `restrict_univ`, `map_iInf_le`, `MeasureTheory.Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict`, `comap_top`, `map_map`, `restrict_empty`, `map_ofFunction`, `map_comap_of_surjective`, `map_iSup`, `restrict_iSup`, `comap_mono`, `le_comap_map`, `MeasureTheory.Measure.map_toOuterMeasure`, `isometryEquiv_map_mkMetric`, `restrict_biInf`, `restrict_sInf_eq_sInf_restrict`, `comap_boundedBy`, `map_id`, `isometry_map_mkMetric`, `map_top_of_surjective`, `restrict_apply`, `map_top`, `restrict_mono`, `comap_iSup`, `map_biInf_comap`, `restrict_iInf_restrict`, `map_ofFunction_le`, `map_sup`, `comap_ofFunction`, `map_mono`, `restrict_le_self`, `isometryEquiv_comap_mkMetric`
`instMulAction` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	30 math math: `le_boundedBy'`, `MeasureTheory.Measure.outerMeasure_le_iff`, `le_pi`, `map_comap_le`, `map_le_restrict_range`, `le_mkMetric`, `map_iInf_le`, `MeasureTheory.le_inducedOuterMeasure`, `trim_le_trim_iff`, `trim_anti_measurableSpace`, `trim_sum_ge`, `comap_mono`, `le_comap_map`, `le_trim`, `mkMetric'.mono_pre_nat`, `le_trim_iff`, `MeasureTheory.Measure.toOuterMeasure_le`, `isGreatest_ofFunction`, `trim_mono`, `mkMetric'.mono_pre`, `instIsOrderedAddMonoid`, `mkMetric_mono`, `MeasureTheory.Measure.trim_le`, `le_boundedBy`, `le_ofFunction`, `map_ofFunction_le`, `map_mono`, `restrict_le_self`, `mkMetric_mono_smul`, `mkMetric'.le_pre`
`instSMul` 📖	CompOp	15 math math: `trim_smul`, `MeasureTheory.Measure.smul_toOuterMeasure`, `instSMulCommClass`, `instIsCentralScalar`, `le_smul_caratheodory`, `smul_boundedBy`, `smul_iSup`, `mkMetric_smul`, `smul_dirac_apply`, `mkMetric_nnreal_smul`, `smul_ofFunction`, `instIsScalarTower`, `coe_smul`, `smul_apply`, `mkMetric_mono_smul`
`instSupSet` 📖	CompOp	10 math math: `coe_iSup`, `map_iSup`, `restrict_iSup`, `sSup_apply`, `smul_iSup`, `mkMetric'.eq_iSup_nat`, `iSup_apply`, `ofFunction_eq_sSup`, `comap_iSup`, `trim_iSup`
`instZero` 📖	CompOp	9 math math: `trim_zero`, `MeasureTheory.Measure.zero_toOuterMeasure`, `restrict_empty`, `zero_caratheodory`, `boundedBy_zero`, `coe_zero`, `coe_bot`, `toMeasure_eq_zero`, `univ_eq_zero_iff`
`map` 📖	CompOp	23 math math: `map_iInf`, `comap_map`, `map_apply`, `map_iInf_comap`, `map_comap_le`, `map_le_restrict_range`, `map_comap`, `map_iInf_le`, `map_map`, `map_ofFunction`, `map_comap_of_surjective`, `map_iSup`, `le_comap_map`, `MeasureTheory.Measure.map_toOuterMeasure`, `isometryEquiv_map_mkMetric`, `map_id`, `isometry_map_mkMetric`, `map_top_of_surjective`, `map_top`, `map_biInf_comap`, `map_ofFunction_le`, `map_sup`, `map_mono`
`orderBot` 📖	CompOp	—
`restrict` 📖	CompOp	18 math math: `map_iInf`, `restrict_trim`, `restrict_iInf`, `restrict_ofFunction`, `map_le_restrict_range`, `map_comap`, `restrict_univ`, `MeasureTheory.Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict`, `restrict_empty`, `restrict_iSup`, `restrict_biInf`, `restrict_sInf_eq_sInf_restrict`, `isometry_map_mkMetric`, `restrict_apply`, `map_top`, `restrict_mono`, `restrict_iInf_restrict`, `restrict_le_self`
`sum` 📖	CompOp	3 math math: `le_sum_caratheodory`, `trim_sum_ge`, `sum_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	—
`coeFnAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `MeasureTheory.OuterMeasure` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `Pi.addZeroClass` `Set` `ENNReal` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `AddMonoidHom.instFunLike` `coeFnAddMonoidHom` `instFunLikeSetENNReal`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `instAdd` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	—
`coe_bot` 📖	mathematical	—	`Bot.bot` `MeasureTheory.OuterMeasure` `instBot` `instZero`	—	—
`coe_iSup` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `iSup` `instSupSet` `Pi.supSet` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`iSup_apply` `iSup_apply`
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `instSMul` `Function.hasSMul`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `instZero` `Pi.instZero` `instZeroENNReal`	—	—
`comap_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `LinearMap` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `comap` `Set.image`	—	`IsScalarTower.right`
`comap_iSup` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.OuterMeasure` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `comap` `iSup` `instSupSet`	—	`ext` `IsScalarTower.right` `iSup_apply`
`comap_map` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.OuterMeasure` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `comap` `map`	—	`ext` `IsScalarTower.right` `comap_apply` `map_apply` `Function.Injective.preimage_image`
`comap_mono` 📖	mathematical	—	`Monotone` `MeasureTheory.OuterMeasure` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `comap`	—	—
`comap_top` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.OuterMeasure` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `comap` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`ext_nonempty` `IsScalarTower.right` `comap_apply` `top_apply` `Set.Nonempty.image`
`dirac_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `dirac` `Set.indicator` `instZeroENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	—
`iSup_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `iSup` `instSupSet` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`iSup.eq_1` `sSup_apply` `iSup_range`
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `MeasureTheory.OuterMeasure` `instSMul` `MulOpposite` `IsScalarTower.op_left` `ENNReal` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	—	`IsScalarTower.op_left` `ext` `IsCentralScalar.op_smul_eq_smul`
`instIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `MeasureTheory.OuterMeasure` `addCommMonoid` `instPartialOrder`	—	`add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `MeasureTheory.OuterMeasure` `instSMul`	—	`ext` `smul_assoc`
`instLawfulFunctor` 📖	mathematical	—	`MeasureTheory.OuterMeasure` `instFunctor`	—	—
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `MeasureTheory.OuterMeasure` `instSMul`	—	`ext` `SMulCommClass.smul_comm`
`le_comap_map` 📖	mathematical	—	`MeasureTheory.OuterMeasure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `comap` `map`	—	`mono` `Set.subset_preimage_image`
`map_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `LinearMap` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `map` `Set.preimage`	—	`IsScalarTower.right`
`map_comap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.OuterMeasure` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `map` `comap` `restrict` `Set.range`	—	`ext` `IsScalarTower.right` `Set.image_preimage_eq_inter_range` `Subtype.range_coe`
`map_comap_le` 📖	mathematical	—	`MeasureTheory.OuterMeasure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `map` `comap`	—	`mono` `Set.image_preimage_subset`
`map_comap_of_surjective` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.OuterMeasure` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `map` `comap`	—	`ext` `IsScalarTower.right` `map_apply` `comap_apply` `Function.Surjective.image_preimage`
`map_iSup` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.OuterMeasure` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `map` `iSup` `instSupSet`	—	`ext` `IsScalarTower.right` `iSup_apply`
`map_id` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.OuterMeasure` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `map`	—	`ext` `IsScalarTower.right`
`map_le_restrict_range` 📖	mathematical	—	`MeasureTheory.OuterMeasure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `map` `restrict` `Set.range`	—	`IsScalarTower.right` `LE.le.trans` `restrict_le_self` `restrict_apply` `Set.preimage_range` `Set.inter_univ`
`map_map` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.OuterMeasure` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `map`	—	`ext` `IsScalarTower.right`
`map_mono` 📖	mathematical	—	`Monotone` `MeasureTheory.OuterMeasure` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `map`	—	—
`map_sup` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.OuterMeasure` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `map` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`ext` `IsScalarTower.right` `sup_apply`
`map_top` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.OuterMeasure` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `map` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `restrict` `Set.range`	—	`ext` `IsScalarTower.right` `map_apply` `restrict_apply` `Set.image_preimage_eq_inter_range` `top_apply'` `Set.image_eq_empty`
`map_top_of_surjective` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.OuterMeasure` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `map` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`IsScalarTower.right` `map_top` `Function.Surjective.range_eq` `restrict_univ`
`mono''` 📖	mathematical	`MeasureTheory.OuterMeasure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Set` `Set.instHasSubset`	`ENNReal` `ENNReal.instPartialOrder` `DFunLike.coe` `instFunLikeSetENNReal`	—	`LE.le.trans` `mono`
`restrict_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `LinearMap` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `restrict` `Set.instInter`	—	`IsScalarTower.right` `Subtype.image_preimage_coe` `Set.inter_comm`
`restrict_empty` 📖	mathematical	—	`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` `Set` `Set.instEmptyCollection` `instZero`	—	`ext` `IsScalarTower.right` `restrict_apply` `Set.inter_empty` `MeasureTheory.measure_empty` `instOuterMeasureClass`
`restrict_iSup` 📖	mathematical	—	`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` `iSup` `instSupSet`	—	`IsScalarTower.right` `comap_iSup` `map_iSup`
`restrict_le_self` 📖	mathematical	—	`MeasureTheory.OuterMeasure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `restrict`	—	`map_comap_le`
`restrict_mono` 📖	mathematical	`Set` `Set.instHasSubset` `MeasureTheory.OuterMeasure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `LinearMap` `ENNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `LinearMap.instFunLike` `restrict`	—	`IsScalarTower.right` `restrict_apply` `LE.le.trans` `mono` `Set.inter_subset_inter_right`
`restrict_univ` 📖	mathematical	—	`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` `Set.univ`	—	`ext` `IsScalarTower.right` `restrict_apply` `Set.inter_univ`
`sSup_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `SupSet.sSup` `instSupSet` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.instMembership`	—	—
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `instSMul`	—	—
`smul_dirac_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `dirac` `Set.indicator` `instZeroENNReal`	—	`IsScalarTower.right` `Set.indicator_mul_right` `mul_one`
`smul_iSup` 📖	mathematical	—	`MeasureTheory.OuterMeasure` `instSMul` `iSup` `instSupSet`	—	`ext` `iSup_apply` `ENNReal.smul_iSup`
`sum_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `sum` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	—	—
`sup_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `ENNReal.instMax`	—	`iSup_apply` `iSup_bool_eq`
`top_apply` 📖	mathematical	`Set.Nonempty`	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `instTopENNReal`	—	`top_unique` `le_trans` `IsScalarTower.right` `smul_dirac_apply` `Set.indicator_of_mem` `le_iSup₂`
`top_apply'` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `iInf` `Set.instEmptyCollection` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `instZeroENNReal`	—	`Set.eq_empty_or_nonempty` `MeasureTheory.measure_empty` `instOuterMeasureClass` `iInf_congr_Prop` `iInf_pos` `top_apply` `Set.Nonempty.ne_empty` `iInf_neg`
`univ_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `Set.univ` `instZeroENNReal` `instZero`	—	`bot_unique` `LE.le.trans_eq` `MeasureTheory.measure_mono` `instOuterMeasureClass` `Set.subset_univ`

---

← Back to Index