OfFunction

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

Statistics

Metric	Count
Definitions boundedBy, ofFunction, sInfGen	3
Theorems biInf_apply, biInf_apply', boundedBy_apply, boundedBy_eq, boundedBy_eq_ofFunction, boundedBy_eq_self, boundedBy_le, boundedBy_top, boundedBy_union_of_top_of_nonempty_inter, boundedBy_zero, comap_boundedBy, comap_iInf, comap_ofFunction, iInf_apply, iInf_apply', iSup_sInfGen_nonempty, isGreatest_ofFunction, le_boundedBy, le_boundedBy', le_ofFunction, map_biInf_comap, map_iInf, map_iInf_comap, map_iInf_le, map_ofFunction, map_ofFunction_le, ofFunction_apply, ofFunction_eq, ofFunction_eq_iInf_mem, ofFunction_eq_sSup, ofFunction_le, ofFunction_union_of_top_of_nonempty_inter, restrict_biInf, restrict_iInf, restrict_iInf_restrict, restrict_ofFunction, restrict_sInf_eq_sInf_restrict, sInfGen_def, sInf_apply, sInf_apply', sInf_eq_boundedBy_sInfGen, smul_boundedBy, smul_ofFunction	43
Total	46

MeasureTheory.OuterMeasure

Definitions

Name	Category	Theorems
boundedBy 📖	CompOp	15 math math: le_boundedBy', boundedBy_caratheodory, boundedBy_eq, boundedBy_le, MeasureTheory.boundedBy_measure, boundedBy_eq_self, boundedBy_zero, boundedBy_apply, boundedBy_top, smul_boundedBy, boundedBy_eq_ofFunction, comap_boundedBy, sInf_eq_boundedBy_sInfGen, boundedBy_union_of_top_of_nonempty_inter, le_boundedBy
ofFunction 📖	CompOp	17 math math: MeasureTheory.AddContent.isCaratheodory_ofFunction_of_mem, restrict_ofFunction, MeasureTheory.AddContent.ofFunction_eq, map_ofFunction, ofFunction_eq_iInf_mem, ofFunction_union_of_top_of_nonempty_inter, isGreatest_ofFunction, boundedBy_eq_ofFunction, ofFunction_le, ofFunction_eq, ofFunction_caratheodory, ofFunction_eq_sSup, le_ofFunction, smul_ofFunction, ofFunction_apply, map_ofFunction_le, comap_ofFunction
sInfGen 📖	CompOp	3 math math: sInf_eq_boundedBy_sInfGen, sInfGen_def, iSup_sInfGen_nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biInf_apply 📖	mathematical	Set.Nonempty	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal instFunLikeSetENNReal iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set.instMembership ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Set.instHasSubset Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	iInf_apply Set.Nonempty.to_subtype iInf_congr_Prop
biInf_apply' 📖	mathematical	Set.Nonempty	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal instFunLikeSetENNReal iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set.instMembership ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Set.instHasSubset Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	iInf_apply' iInf_congr_Prop
boundedBy_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal instFunLikeSetENNReal boundedBy iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Set.instHasSubset Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace iSup Set.Nonempty ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup SummationFilter.unconditional	—	—
boundedBy_eq 📖	mathematical	Set Set.instEmptyCollection ENNReal instZeroENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	DFunLike.coe MeasureTheory.OuterMeasure instFunLikeSetENNReal boundedBy	—	boundedBy_eq_ofFunction ofFunction_eq
boundedBy_eq_ofFunction 📖	mathematical	Set Set.instEmptyCollection ENNReal instZeroENNReal	DFunLike.coe MeasureTheory.OuterMeasure instFunLikeSetENNReal boundedBy ofFunction	—	Set.eq_empty_or_nonempty iSup_congr_Prop iSup_neg bot_eq_zero' ENNReal.instCanonicallyOrderedAdd iSup_pos ofFunction.congr_simp
boundedBy_eq_self 📖	mathematical	—	boundedBy DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal instFunLikeSetENNReal	—	ext boundedBy_eq MeasureTheory.measure_empty instOuterMeasureClass MeasureTheory.measure_mono MeasureTheory.measure_iUnion_le instCountableNat
boundedBy_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.OuterMeasure Set instFunLikeSetENNReal boundedBy	—	LE.le.trans ofFunction_le iSup_const_le
boundedBy_top 📖	mathematical	—	boundedBy Top.top Pi.instTopForall Set ENNReal instTopENNReal MeasureTheory.OuterMeasure OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	eq_top_iff le_boundedBy' top_apply le_rfl
boundedBy_union_of_top_of_nonempty_inter 📖	mathematical	Top.top ENNReal instTopENNReal	DFunLike.coe MeasureTheory.OuterMeasure Set instFunLikeSetENNReal boundedBy Set.instUnion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	ofFunction_union_of_top_of_nonempty_inter top_unique LE.le.trans Eq.ge le_iSup Set.Nonempty.mono Set.inter_subset_right
boundedBy_zero 📖	mathematical	—	boundedBy Pi.instZero Set ENNReal instZeroENNReal MeasureTheory.OuterMeasure instZero	—	coe_bot eq_bot_iff boundedBy_le
comap_boundedBy 📖	mathematical	Monotone Set Set.Nonempty ENNReal Subtype.preorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ENNReal.instPartialOrder	DFunLike.coe LinearMap CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.OuterMeasure addCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike comap boundedBy Set.image	—	IsScalarTower.right comap_ofFunction iSup_le Set.Nonempty.mono LE.le.trans le_iSup Set.image_nonempty
comap_iInf 📖	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 iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	ext_nonempty IsScalarTower.right LE.le.antisymm Monotone.map_iInf_le comap_mono iInf_apply' iInf_congr_Prop Set.Nonempty.image Set.preimage_iUnion iInf_le_of_le ENNReal.tsum_le_tsum iInf_mono mono Set.image_preimage_subset
comap_ofFunction 📖	mathematical	Set Set.instEmptyCollection ENNReal instZeroENNReal Monotone PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ENNReal.instPartialOrder	DFunLike.coe LinearMap CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.OuterMeasure addCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike comap ofFunction Set.image	—	le_antisymm IsScalarTower.right le_ofFunction comap_apply ofFunction_le ofFunction_apply iInf_mono' Set.preimage_iUnion Set.image_subset_iff ENNReal.tsum_le_tsum Set.image_preimage_subset Eq.le Function.Surjective.image_preimage
iInf_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal instFunLikeSetENNReal iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Set.instHasSubset Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	iInf.eq_1 sInf_apply Set.range_nonempty iInf_congr_Prop iInf_range
iInf_apply' 📖	mathematical	Set.Nonempty	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal instFunLikeSetENNReal iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Set.instHasSubset Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	iInf.eq_1 sInf_apply' iInf_congr_Prop iInf_range
iSup_sInfGen_nonempty 📖	mathematical	Set.Nonempty MeasureTheory.OuterMeasure	iSup ENNReal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder sInfGen iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set Set.instMembership DFunLike.coe instFunLikeSetENNReal	—	Set.eq_empty_or_nonempty iSup_congr_Prop iSup_neg bot_eq_zero' ENNReal.instCanonicallyOrderedAdd iInf_congr_Prop MeasureTheory.measure_empty instOuterMeasureClass biInf_const iSup_pos
isGreatest_ofFunction 📖	mathematical	Set Set.instEmptyCollection ENNReal instZeroENNReal	IsGreatest MeasureTheory.OuterMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder setOf ofFunction	—	ofFunction_le le_ofFunction
le_boundedBy 📖	mathematical	—	MeasureTheory.OuterMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder boundedBy ENNReal ENNReal.instPartialOrder DFunLike.coe Set instFunLikeSetENNReal	—	boundedBy.eq_1 le_ofFunction Set.eq_empty_or_nonempty MeasureTheory.measure_empty instOuterMeasureClass iSup_congr_Prop iSup_neg bot_eq_zero' ENNReal.instCanonicallyOrderedAdd iSup_pos
le_boundedBy' 📖	mathematical	—	MeasureTheory.OuterMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder boundedBy ENNReal ENNReal.instPartialOrder DFunLike.coe Set instFunLikeSetENNReal	—	le_boundedBy Set.eq_empty_or_nonempty MeasureTheory.measure_empty instOuterMeasureClass ENNReal.instCanonicallyOrderedAdd
le_ofFunction 📖	mathematical	Set Set.instEmptyCollection ENNReal instZeroENNReal	MeasureTheory.OuterMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder ofFunction ENNReal.instPartialOrder DFunLike.coe instFunLikeSetENNReal	—	le_trans ofFunction_le le_iInf mono MeasureTheory.measure_iUnion_le instOuterMeasureClass instCountableNat ENNReal.tsum_le_tsum
map_biInf_comap 📖	mathematical	Set.Nonempty	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 iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set Set.instMembership comap	—	IsScalarTower.right iInf_subtype'' map_iInf_comap Set.Nonempty.to_subtype
map_iInf 📖	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 iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice restrict Set.range	—	IsScalarTower.right comap_iInf comap_map map_comap
map_iInf_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 iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice comap	—	LE.le.antisymm IsScalarTower.right map_iInf_le iInf_apply iInf_congr_Prop iInf_le_of_le Set.iUnion_union Set.union_comm Set.inter_subset Set.image_iUnion Set.image_preimage_eq_inter_range Set.image_mono ENNReal.tsum_le_tsum iInf_mono mono Set.preimage_range Set.compl_univ Set.union_empty subset_rfl Set.instReflSubset
map_iInf_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 iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	Monotone.map_iInf_le IsScalarTower.right map_mono
map_ofFunction 📖	mathematical	Set Set.instEmptyCollection ENNReal instZeroENNReal	DFunLike.coe LinearMap CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.OuterMeasure addCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike map ofFunction Set.preimage	—	LE.le.antisymm IsScalarTower.right map_ofFunction_le iInf_le_of_le Set.union_iUnion Set.inter_subset Set.image_preimage_eq_inter_range Set.image_iUnion Set.image_mono ENNReal.tsum_le_tsum le_of_eq Set.preimage_range Set.compl_univ Function.Injective.preimage_image Set.empty_union
map_ofFunction_le 📖	mathematical	Set Set.instEmptyCollection ENNReal instZeroENNReal	MeasureTheory.OuterMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder DFunLike.coe LinearMap CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring addCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike map ofFunction Set.preimage	—	IsScalarTower.right le_ofFunction map_apply ofFunction_le
ofFunction_apply 📖	mathematical	Set Set.instEmptyCollection ENNReal instZeroENNReal	DFunLike.coe MeasureTheory.OuterMeasure instFunLikeSetENNReal ofFunction iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Set.instHasSubset Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	—
ofFunction_eq 📖	mathematical	Set Set.instEmptyCollection ENNReal instZeroENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	DFunLike.coe MeasureTheory.OuterMeasure instFunLikeSetENNReal ofFunction	—	le_antisymm ofFunction_le le_iInf le_trans
ofFunction_eq_iInf_mem 📖	mathematical	Set Set.instEmptyCollection ENNReal instZeroENNReal Top.top instTopENNReal	DFunLike.coe MeasureTheory.OuterMeasure instFunLikeSetENNReal ofFunction iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Set.instHasSubset Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	ofFunction_apply le_antisymm le_iInf iInf₂_le iInf_le_of_le le_rfl iInf_congr_Prop iInf_neg Mathlib.Tactic.Push.not_forall_eq ENNReal.tsum_eq_top_of_eq_top
ofFunction_eq_sSup 📖	mathematical	Set Set.instEmptyCollection ENNReal instZeroENNReal	ofFunction SupSet.sSup MeasureTheory.OuterMeasure instSupSet setOf	—	IsLUB.sSup_eq IsGreatest.isLUB isGreatest_ofFunction
ofFunction_le 📖	mathematical	Set Set.instEmptyCollection ENNReal instZeroENNReal	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.OuterMeasure instFunLikeSetENNReal ofFunction	—	iInf_le_of_le Set.subset_iUnion le_of_eq tsum_eq_single SummationFilter.instLeAtTopUnconditional instIsEmptyFalse
ofFunction_union_of_top_of_nonempty_inter 📖	mathematical	Set Set.instEmptyCollection ENNReal instZeroENNReal Top.top instTopENNReal	DFunLike.coe MeasureTheory.OuterMeasure instFunLikeSetENNReal ofFunction Set.instUnion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	le_antisymm MeasureTheory.measure_union_le instOuterMeasureClass le_iInf₂ le_top ENNReal.le_tsum disjoint_iff_inf_le mono Set.mem_iUnion MeasureTheory.measure_iUnion_le SetCoe.countable instCountableNat add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Set.subset_union_left Set.subset_union_right Summable.tsum_union_disjoint ENNReal.instT2Space ENNReal.instContinuousAdd ENNReal.summable OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Subtype.coe_injective zero_le ENNReal.instCanonicallyOrderedAdd le_rfl ENNReal.tsum_le_tsum ofFunction_le
restrict_biInf 📖	mathematical	Set.Nonempty	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 iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set Set.instMembership	—	IsScalarTower.right iInf_subtype'' restrict_iInf Set.Nonempty.to_subtype
restrict_iInf 📖	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 iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	IsScalarTower.right comap_iInf map_iInf_comap
restrict_iInf_restrict 📖	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 iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	IsScalarTower.right Subtype.range_coe map_iInf Subtype.coe_injective comap_iInf
restrict_ofFunction 📖	mathematical	Set Set.instEmptyCollection ENNReal instZeroENNReal Monotone PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ENNReal.instPartialOrder	DFunLike.coe LinearMap CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.OuterMeasure addCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike restrict ofFunction Set.instInter	—	IsScalarTower.right restrict.eq_1 Set.inter_comm ofFunction.congr_simp comap_ofFunction Subtype.image_preimage_coe map_ofFunction Subtype.coe_injective
restrict_sInf_eq_sInf_restrict 📖	mathematical	Set.Nonempty MeasureTheory.OuterMeasure	DFunLike.coe LinearMap ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring addCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike restrict InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set.image	—	IsScalarTower.right sInf_eq_iInf restrict_biInf iInf_image
sInfGen_def 📖	mathematical	—	sInfGen iInf ENNReal MeasureTheory.OuterMeasure ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Set Set.instMembership DFunLike.coe instFunLikeSetENNReal	—	—
sInf_apply 📖	mathematical	Set.Nonempty MeasureTheory.OuterMeasure	DFunLike.coe Set ENNReal instFunLikeSetENNReal InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice iInf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Set.instHasSubset Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace Set.instMembership SummationFilter.unconditional	—	sInf_eq_boundedBy_sInfGen boundedBy_apply iInf_congr_Prop iSup_sInfGen_nonempty
sInf_apply' 📖	mathematical	Set.Nonempty	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal instFunLikeSetENNReal InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice iInf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Set.instHasSubset Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace Set.instMembership SummationFilter.unconditional	—	Set.eq_empty_or_nonempty sInf_empty top_apply iInf_congr_Prop iInf_neg iInf_top ENNReal.tsum_top sInf_apply
sInf_eq_boundedBy_sInfGen 📖	mathematical	—	InfSet.sInf MeasureTheory.OuterMeasure ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice boundedBy sInfGen	—	le_antisymm le_boundedBy le_iInf₂ sInf_le le_sInf le_trans boundedBy_le iInf₂_le
smul_boundedBy 📖	mathematical	—	ENNReal MeasureTheory.OuterMeasure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right boundedBy Function.hasSMul Set	—	IsScalarTower.right smul_ofFunction Set.eq_empty_or_nonempty iSup_congr_Prop iSup_neg bot_eq_zero' ENNReal.instCanonicallyOrderedAdd MulZeroClass.mul_zero iSup_pos
smul_ofFunction 📖	mathematical	Set Set.instEmptyCollection ENNReal instZeroENNReal	MeasureTheory.OuterMeasure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right ofFunction Function.hasSMul	—	ext IsScalarTower.right iInf_subtype' iInf_congr_Prop ENNReal.tsum_mul_left ENNReal.mul_iInf Set.subset_iUnion

---

← Back to Index