SmoothingSeminorm

📁 Source: Mathlib/Analysis/Normed/Unbundled/SmoothingSeminorm.lean

Statistics

Metric	Count
Definitions smoothingFun, smoothingSeminorm, smoothingSeminormSeq	3
Theorems isNonarchimedean_smoothingFun, isPowMul_smoothingFun, smoothingFun_apply_of_map_mul_eq_mul, smoothingFun_le, smoothingFun_le_self, smoothingFun_nonneg, smoothingFun_of_map_mul_eq_mul, smoothingFun_of_powMul, smoothingFun_one_le, smoothingSeminormSeq_bddBelow, smoothingSeminorm_apply_of_map_mul_eq_mul, smoothingSeminorm_map_one_le_one, smoothingSeminorm_of_mul, tendsto_smoothingFun_comp, tendsto_smoothingFun_of_eq_zero, tendsto_smoothingFun_of_map_one_le_one, tendsto_smoothingFun_of_ne_zero, zero_mem_lowerBounds_smoothingSeminormSeq_range	18
Total	21

(root)

Definitions

Name	Category	Theorems
smoothingFun 📖	CompOp	13 math math: tendsto_smoothingFun_of_ne_zero, smoothingFun_of_powMul, tendsto_smoothingFun_comp, isPowMul_smoothingFun, smoothingFun_le, smoothingFun_nonneg, tendsto_smoothingFun_of_map_one_le_one, smoothingFun_apply_of_map_mul_eq_mul, smoothingFun_le_self, smoothingFun_of_map_mul_eq_mul, isNonarchimedean_smoothingFun, tendsto_smoothingFun_of_eq_zero, smoothingFun_one_le
smoothingSeminorm 📖	CompOp	3 math math: smoothingSeminorm_apply_of_map_mul_eq_mul, smoothingSeminorm_map_one_le_one, smoothingSeminorm_of_mul
smoothingSeminormSeq 📖	CompOp	3 math math: tendsto_smoothingFun_of_ne_zero, tendsto_smoothingFun_of_map_one_le_one, tendsto_smoothingFun_of_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNonarchimedean_smoothingFun 📖	mathematical	Real Real.instLE DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne IsNonarchimedean Real.linearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	smoothingFun	—	RingSeminorm.exists_index_pow_le Metric.isBounded_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal tendsto_subseq_of_bounded instProperSpaceReal Filter.Tendsto.congr' instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Nat.cast_ne_zero RCLike.charZero_rclike ne_of_gt lt_of_le_of_lt zero_le Nat.instCanonicallyOrderedAdd div_self sub_div Nat.cast_sub Filter.Tendsto.const_sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Set.Icc.mem_iff_one_sub_mem Real.instIsOrderedRing closure_Icc HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Nat.instOrderedSub limsup_mul_le Filter.Frequently.of_forall Filter.atTop_neBot Real.rpow_nonneg NonnegHomClass.apply_nonneg RingSeminormClass.toNonnegHomClass RingSeminorm.ringSeminormClass BddAbove.isBoundedUnder_of_range Filter.Eventually.of_forall RingSeminorm.isBoundedUnder le_trans mul_le_mul IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono Filter.le_limsup_of_frequently_le smoothingFun_nonneg le_of_forall_sub_le Real.instIsStrictOrderedRing sub_le_iff_le_add covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono max_def add_le_add_iff_right IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le mul_le_mul_of_nonneg_right Real.rpow_le_rpow Real.rpow_add_of_nonneg sub_nonneg add_sub add_sub_cancel_left Real.rpow_one le_refl mul_le_mul_of_nonneg_left le_of_lt not_le Filter.exists_lt_of_limsup_le IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd bddAbove_range_mul StrictMono.lt_iff_lt PNat.pos ciInf_le smoothingSeminormSeq_bddBelow one_div Real.mul_rpow LT.lt.le
isPowMul_smoothingFun 📖	mathematical	Real Real.instLE DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne	IsPowMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring smoothingFun	—	Filter.Tendsto.comp tendsto_smoothingFun_of_map_one_le_one Filter.tendsto_atTop_atTop_of_monotone mul_le_mul_right Nat.instMulLeftMono le_mul_of_one_le_left' covariant_swap_mul_of_covariant_mul tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Nat.cast_ne_zero RCLike.charZero_rclike ne_of_gt lt_of_lt_of_le zero_lt_one Nat.instZeroLEOneClass pow_mul Real.rpow_natCast Real.rpow_mul NonnegHomClass.apply_nonneg RingSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid RingSeminorm.ringSeminormClass Nat.cast_mul one_div_mul_one_div mul_comm mul_assoc one_div_mul_cancel mul_one Filter.Tendsto.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal
smoothingFun_apply_of_map_mul_eq_mul 📖	mathematical	Real Real.instLE DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Real.instMul	smoothingFun	—	tendsto_nhds_unique_of_eventuallyEq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_smoothingFun_of_map_one_le_one tendsto_const_nhds le_antisymm le_trans map_pow_le_pow RingSeminorm.ringSeminormClass zero_pow pos_iff_ne_zero Nat.instCanonicallyOrderedAdd le_refl NonnegHomClass.apply_nonneg RingSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid Real.zero_rpow Nat.one_div_cast_ne_zero Real.instIsStrictOrderedRing mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain mul_one Nat.cast_ne_zero RCLike.charZero_rclike ne_of_gt lt_of_lt_of_le zero_lt_one Nat.instZeroLEOneClass pow_mul_apply_eq_pow_mul Real.rpow_natCast Real.rpow_mul mul_one_div_cancel Real.rpow_one
smoothingFun_le 📖	mathematical	—	Real Real.instLE smoothingFun Real.instPow DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring PNat.val DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instNatCast	—	ciInf_le smoothingSeminormSeq_bddBelow
smoothingFun_le_self 📖	mathematical	—	Real Real.instLE smoothingFun DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing	—	LE.le.trans smoothingFun_le PNat.one_coe pow_one Nat.cast_one div_one Real.rpow_one le_refl
smoothingFun_nonneg 📖	mathematical	Real Real.instLE DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne	Real.instZero smoothingFun	—	ge_of_tendsto instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_smoothingFun_of_map_one_le_one Real.rpow_nonneg NonnegHomClass.apply_nonneg RingSeminormClass.toNonnegHomClass RingSeminorm.ringSeminormClass
smoothingFun_of_map_mul_eq_mul 📖	mathematical	Real Real.instLE DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Real.instMul	smoothingFun	—	smoothingFun_apply_of_map_mul_eq_mul Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_smoothingFun_of_map_one_le_one tendsto_nhds_unique_of_eventuallyEq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Nat.cast_ne_zero RCLike.charZero_rclike ne_of_gt lt_of_lt_of_le zero_lt_one Nat.instZeroLEOneClass mul_pow pow_mul_apply_eq_pow_mul Real.mul_rpow pow_nonneg Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing NonnegHomClass.apply_nonneg RingSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid RingSeminorm.ringSeminormClass Real.rpow_natCast Real.rpow_mul mul_one_div_cancel Real.rpow_one
smoothingFun_of_powMul 📖	mathematical	Real Real.instLE DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Real.instMonoid	smoothingFun	—	tendsto_nhds_unique_of_eventuallyEq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_smoothingFun_of_map_one_le_one tendsto_const_nhds Nat.cast_ne_zero RCLike.charZero_rclike Real.rpow_natCast Real.rpow_mul NonnegHomClass.apply_nonneg RingSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid RingSeminorm.ringSeminormClass mul_one_div_cancel Real.rpow_one
smoothingFun_one_le 📖	mathematical	Real Real.instLE DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne	smoothingFun	—	le_of_tendsto instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_smoothingFun_of_map_one_le_one one_pow Real.one_rpow div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Nat.cast_zero Nat.cast_lt IsOrderedAddMonoid.toAddLeftMono Real.rpow_le_rpow_iff NonnegHomClass.apply_nonneg RingSeminormClass.toNonnegHomClass RingSeminorm.ringSeminormClass zero_le_one
smoothingSeminormSeq_bddBelow 📖	mathematical	—	BddBelow Real Real.instLE Set.range PNat Real.instPow DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring PNat.val DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instNatCast	—	zero_mem_lowerBounds_smoothingSeminormSeq_range
smoothingSeminorm_apply_of_map_mul_eq_mul 📖	mathematical	Real Real.instLE DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne IsNonarchimedean Real.linearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toMul Real.instMul	smoothingSeminorm	—	smoothingFun_apply_of_map_mul_eq_mul
smoothingSeminorm_map_one_le_one 📖	mathematical	Real Real.instLE DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne IsNonarchimedean Real.linearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	smoothingSeminorm	—	smoothingFun_one_le
smoothingSeminorm_of_mul 📖	mathematical	Real Real.instLE DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne IsNonarchimedean Real.linearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toMul Real.instMul	smoothingSeminorm	—	smoothingFun_of_map_mul_eq_mul
tendsto_smoothingFun_comp 📖	mathematical	Real Real.instLE DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne StrictMono Nat.instPreorder	Filter.Tendsto Real.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace smoothingFun	—	StrictMono.tendsto_atTop Filter.Tendsto.comp tendsto_smoothingFun_of_map_one_le_one
tendsto_smoothingFun_of_eq_zero 📖	mathematical	DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing Real.instZero	Filter.Tendsto smoothingSeminormSeq Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace smoothingFun	—	le_antisymm zero_pow pos_iff_ne_zero Nat.instCanonicallyOrderedAdd map_pow_le_pow RingSeminorm.ringSeminormClass NonnegHomClass.apply_nonneg RingSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid Real.zero_rpow Nat.one_div_cast_ne_zero Real.instIsStrictOrderedRing ciInf_le_of_le smoothingSeminormSeq_bddBelow le_of_eq le_refl le_ciInf Real.rpow_nonneg tendsto_atTop_of_eventually_const
tendsto_smoothingFun_of_map_one_le_one 📖	mathematical	Real Real.instLE DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne	Filter.Tendsto smoothingSeminormSeq Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace smoothingFun	—	tendsto_smoothingFun_of_eq_zero tendsto_smoothingFun_of_ne_zero
tendsto_smoothingFun_of_ne_zero 📖	mathematical	Real Real.instLE DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne	Filter.Tendsto smoothingSeminormSeq Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace smoothingFun	—	le_ciInf Real.rpow_nonneg NonnegHomClass.apply_nonneg RingSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid RingSeminorm.ringSeminormClass Metric.tendsto_atTop Nat.instAtLeastTwoHAddOfNat half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing PNat.pos div_mul_eq_div_mul_one_div mul_pos inv_pos_of_pos add_pos_of_nonneg_of_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono one_div le_of_lt abs_lt covariant_swap_add_of_covariant_add Real.dist_eq lt_of_lt_of_le le_max_left PNat.mk_coe ciInf_le smoothingSeminormSeq_bddBelow neg_lt_zero sub_nonneg lt_of_le_of_lt pow_add MulZeroClass.mul_zero Real.zero_rpow Nat.one_div_cast_ne_zero pos_iff_ne_zero Nat.instCanonicallyOrderedAdd Real.mul_rpow Real.rpow_le_rpow SubmultiplicativeHomClass.map_mul_le_mul RingSeminormClass.toSubmultiplicativeHomClass Nat.one_div_cast_nonneg lt_of_le_of_ne pow_mul map_pow_le_pow le_trans Nat.cast_ne_zero RCLike.charZero_rclike ne_of_gt Real.rpow_one div_self div_pos Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial Real.rpow_natCast Real.rpow_add neg_div add_div Nat.cast_add add_neg_cancel_right Nat.cast_mul Real.rpow_mul mul_one_div mul_div_assoc Real.rpow_lt_rpow one_div_mul_cancel Real.rpow_lt_rpow_iff pow_zero Real.one_rpow add_assoc add_halves CharZero.NeZero.two tsub_le_iff_left AddGroup.toOrderedSub mul_one mul_assoc mul_sub mul_comm le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono div_div le_max_right Real.rpow_pos_of_pos mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono lt_of_le_of_ne' mul_lt_mul_of_pos_right mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Right.add_pos_of_nonneg_of_pos Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo tsub_lt_iff_left AddGroup.existsAddOfLE IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le
zero_mem_lowerBounds_smoothingSeminormSeq_range 📖	mathematical	—	Real Set Set.instMembership lowerBounds Real.instLE Set.range PNat Real.instPow DFunLike.coe RingSeminorm NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring PNat.val DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instNatCast Real.instZero	—	Real.rpow_nonneg NonnegHomClass.apply_nonneg RingSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid RingSeminorm.ringSeminormClass

---

← Back to Index