Gauge

📁 Source: Mathlib/Analysis/Convex/Gauge.lean

Statistics

Metric	Count
Definitions gauge, gaugeSeminorm	2
Theorems gauge_set_nonempty, starConvex, gauge_le, lipschitzWith_gauge, lipschitz_gauge, uniformContinuous_gauge, gaugeSeminorm_ball, gauge_ball, comap_gauge_nhds_zero, comap_gauge_nhds_zero_le, continuousAt_gauge, continuousAt_gauge_zero, continuous_gauge, exists_lt_of_gauge_lt, gaugeSeminorm_ball_one, gaugeSeminorm_lt_one_of_isOpen, gaugeSeminorm_toFun, gauge_add_le, gauge_ball, gauge_closedBall, gauge_closure_zero, gauge_def, gauge_def', gauge_empty, gauge_eq_one_iff_mem_frontier, gauge_eq_zero, gauge_le_eq, gauge_le_of_mem, gauge_le_one_iff_mem_closure, gauge_le_one_of_mem, gauge_lt_eq, gauge_lt_eq', gauge_lt_of_mem_smul, gauge_lt_one_eq_interior, gauge_lt_one_eq_self_of_isOpen, gauge_lt_one_iff_mem_interior, gauge_lt_one_of_mem_of_isOpen, gauge_lt_one_subset_self, gauge_mono, gauge_neg, gauge_neg_set_eq_gauge_neg, gauge_neg_set_neg, gauge_nonneg, gauge_norm_smul, gauge_of_subset_zero, gauge_pos, gauge_smul, gauge_smul_left, gauge_smul_left_of_nonneg, gauge_smul_of_nonneg, gauge_sum_le, gauge_unit_ball, gauge_zero, gauge_zero', interior_subset_gauge_lt_one, le_gauge_of_notMem, le_gauge_of_subset_closedBall, mem_closure_of_gauge_le_one, mem_frontier_of_gauge_eq_one, mem_openSegment_of_gauge_lt_one, mul_gauge_le_norm, one_le_gauge_of_notMem, self_subset_gauge_le_one, tendsto_gauge_nhds_zero, tendsto_gauge_nhds_zero_nhdsGE	65
Total	67

Absorbent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gauge_set_nonempty 📖	mathematical	Absorbent Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid	Set.Nonempty setOf Real.instLT Real.instZero Set Set.instMembership Set.smulSet	—	Absorbs.exists_pos Eq.ge Real.norm_of_nonneg LT.lt.le

Balanced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
starConvex 📖	mathematical	Balanced Real SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid	StarConvex Real.partialOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	starConvex_zero_iff covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.norm_of_nonneg Set.smul_mem_smul_set

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gauge_le 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Absorbent PseudoMetricSpace.toBornology Real.pseudoMetricSpace	setOf Real.instLE gauge	—	gauge_le_eq convex_iInter smul Set.eq_empty_iff_forall_notMem LE.le.trans gauge_nonneg convex_empty
lipschitzWith_gauge 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal Set Set.instHasSubset Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NNReal.toReal	LipschitzWith PseudoMetricSpace.toPseudoEMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace NNReal.instInv gauge	—	absorbent_ball_zero LipschitzWith.of_le_add_mul add_sub_cancel gauge_add_le Absorbent.mono le_imp_le_of_le_of_le add_le_add_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid gauge_mono le_refl gauge_ball le_of_lt Mathlib.Meta.Positivity.nnreal_coe_pos dist_eq_norm div_eq_inv_mul NNReal.coe_inv
lipschitz_gauge 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	LipschitzWith PseudoMetricSpace.toPseudoEMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace gauge	—	Metric.mem_nhds_iff LT.lt.le lipschitzWith_gauge
uniformContinuous_gauge 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	UniformContinuous Real.pseudoMetricSpace gauge	—	lipschitz_gauge LipschitzWith.uniformContinuous

Seminorm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gaugeSeminorm_ball 📖	mathematical	—	gaugeSeminorm Real ball SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instOne Real.instRCLike IsScalarTower.left DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Real.normedField DistribMulAction.toMulAction AddCommMonoid.toAddMonoid balanced_ball_zero convex_ball NormedField.toNormedSpace Real.instMonoid Real.semiring absorbent_ball_zero zero_lt_one Real.instZero Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing RCLike.charZero_rclike	—	DFunLike.coe_injective IsScalarTower.left balanced_ball_zero convex_ball absorbent_ball_zero zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike gauge_ball
gauge_ball 📖	mathematical	—	gauge ball Real SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instOne DFunLike.coe Seminorm instFunLike	—	Set.eq_empty_or_nonempty gauge.eq_1 Real.sInf_empty LE.le.lt_of_ne NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass instSeminormClass Nat.instAtLeastTwoHAddOfNat mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Eq.subset Set.instReflSubset mem_ball_zero SeminormClass.map_smul_eq_mul Real.norm_eq_abs abs_of_pos inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE inv_mul_lt_iff₀ mul_one lt_mul_of_one_lt_left IsStrictOrderedRing.toMulPosStrictMono one_lt_two IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd smul_inv_smul₀ LT.lt.ne' IsGLB.csInf_eq mul_le_of_le_one_right IsOrderedRing.toPosMulMono Real.instIsOrderedRing LT.lt.le le_of_forall_pos_le_add LinearOrderedSemiField.toDenselyOrdered AddGroup.existsAddOfLE contravariant_lt_of_covariant_le Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add lt_add_of_pos_right

(root)

Definitions

Name	Category	Theorems
gauge 📖	CompOp	60 math math: gauge_lt_one_eq_self_of_isOpen, comap_gauge_nhds_zero_le, gauge_def', gauge_le_one_of_mem, gauge_lt_one_of_mem_of_isOpen, gauge_smul_of_nonneg, gauge_gaugeRescale, gauge_le_of_mem, le_gauge_of_notMem, gauge_le_eq, gauge_neg, gauge_zero', gauge_eq_zero, gauge_norm_smul, gauge_lt_of_mem_smul, Convex.uniformContinuous_gauge, gauge_closure_zero, gauge_ball, interior_subset_gauge_lt_one, mul_gauge_le_norm, gauge_empty, gauge_eq_one_iff_mem_frontier, one_le_gauge_of_notMem, continuous_gauge, gauge_of_subset_zero, gauge_smul_left_of_nonneg, gauge_pos, gauge_def, continuousAt_gauge_zero, continuousAt_gauge, self_subset_gauge_le_one, gauge_lt_one_subset_self, tendsto_gauge_nhds_zero_nhdsGE, Convex.gauge_le, gauge_gaugeRescale', gauge_unit_ball, tendsto_gauge_nhds_zero, gauge_nonneg, gauge_mono, gauge_neg_set_eq_gauge_neg, gaugeRescale_def, Convex.lipschitz_gauge, gauge_lt_one_eq_interior, gauge_sum_le, Seminorm.gauge_ball, gauge_lt_eq', comap_gauge_nhds_zero, gauge_le_one_iff_mem_closure, Convex.lipschitzWith_gauge, gauge_gaugeRescale_le, gauge_neg_set_neg, gauge_smul, gauge_lt_one_iff_mem_interior, gauge_smul_left, gauge_add_le, gauge_lt_eq, le_gauge_of_subset_closedBall, gauge_closedBall, gauge_zero, gaugeSeminorm_toFun
gaugeSeminorm 📖	CompOp	4 math math: Seminorm.gaugeSeminorm_ball, gaugeSeminorm_ball_one, gaugeSeminorm_lt_one_of_isOpen, gaugeSeminorm_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_gauge_nhds_zero 📖	mathematical	Bornology.IsVonNBounded Real SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set Filter Filter.instMembership nhds	Filter.comap gauge UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	LE.le.antisymm comap_gauge_nhds_zero_le absorbent_nhds_zero Filter.Tendsto.le_comap tendsto_gauge_nhds_zero
comap_gauge_nhds_zero_le 📖	mathematical	Absorbent Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.comap gauge nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.instZero	—	Absorbs.exists_pos Filter.mp_mem Filter.preimage_mem_comap gt_mem_nhds instOrderTopologyReal inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Filter.univ_mem' exists_lt_of_gauge_lt lt_inv_comm₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono LE.le.trans LT.lt.le le_abs_self smul_inv_smul₀ LT.lt.ne'
continuousAt_gauge 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace gauge	—	absorbent_nhds_zero Filter.HasBasis.tendsto_right_iff nhds_basis_Icc_pos Real.instIsOrderedAddMonoid instOrderTopologyReal instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing map_add_left_nhds_zero Filter.eventually_map Filter.inter_mem set_smul_mem_nhds_zero_iff ContinuousSMul.continuousConstSMul LT.lt.ne' neg_mem_nhds_zero Filter.mp_mem Filter.univ_mem' sub_le_iff_le_add covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono add_neg_cancel_right gauge_add_le le_imp_le_of_le_of_le add_le_add_right gauge_le_of_mem LT.lt.le Set.mem_neg le_refl
continuousAt_gauge_zero 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace gauge	—	ContinuousAt.eq_1 gauge_zero tendsto_gauge_nhds_zero
continuous_gauge 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace gauge	—	continuous_iff_continuousAt continuousAt_gauge
exists_lt_of_gauge_lt 📖	mathematical	Absorbent Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid Real.instLT gauge	Real.instZero Set Set.instMembership Set.smulSet	—	exists_lt_of_csInf_lt Absorbent.gauge_set_nonempty
gaugeSeminorm_ball_one 📖	mathematical	Balanced SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Convex Real Real.semiring Real.partialOrder Real.instMonoid Absorbent PseudoMetricSpace.toBornology Real.pseudoMetricSpace IsOpen	Seminorm.ball gaugeSeminorm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instOne	—	Seminorm.ball_zero_eq gauge_lt_one_eq_self_of_isOpen Absorbent.zero_mem NontriviallyNormedField.cobounded_neBot
gaugeSeminorm_lt_one_of_isOpen 📖	mathematical	Balanced SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Convex Real Real.semiring Real.partialOrder Real.instMonoid Absorbent PseudoMetricSpace.toBornology Real.pseudoMetricSpace IsOpen Set Set.instMembership	Real.instLT DFunLike.coe Seminorm Seminorm.instFunLike gaugeSeminorm Real.instOne	—	gauge_lt_one_of_mem_of_isOpen
gaugeSeminorm_toFun 📖	mathematical	Balanced SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Convex Real Real.semiring Real.partialOrder Real.instMonoid Absorbent PseudoMetricSpace.toBornology Real.pseudoMetricSpace	DFunLike.coe Seminorm Seminorm.instFunLike gaugeSeminorm gauge	—	—
gauge_add_le 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Absorbent PseudoMetricSpace.toBornology Real.pseudoMetricSpace	Real.instLE gauge AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Real.instAdd	—	le_of_forall_pos_lt_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.instAtLeastTwoHAddOfNat exists_lt_of_gauge_lt lt_add_of_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing gauge_le_of_mem le_of_lt add_pos' Convex.add_smul LT.lt.le Set.add_mem_add Set.smul_mem_smul_set lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.add_neg CancelDenoms.sub_subst CancelDenoms.add_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le
gauge_ball 📖	mathematical	Real Real.instLE Real.instZero	gauge SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm SeminormedAddCommGroup.toNorm	—	LE.le.eq_or_lt Metric.ball_zero gauge_empty div_zero smul_unitBall_of_pos gauge_smul_left Real.instIsStrictOrderedRing IsStrictOrderedRing.toIsStrictOrderedModule Algebra.to_smulCommClass IsScalarTower.right IsScalarTower.left norm_neg Pi.smul_apply gauge_unit_ball smul_eq_mul abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le div_eq_inv_mul
gauge_closedBall 📖	mathematical	Real Real.instLE Real.instZero	gauge SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm SeminormedAddCommGroup.toNorm	—	LE.le.eq_or_lt div_zero Metric.closedBall_zero' Set.singleton_zero gauge_closure_zero le_antisymm gauge_ball gauge_mono absorbent_ball_zero Metric.ball_subset_closedBall Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' LE.le.trans LT.lt.le Membership.mem.out Absorbent.mono Metric.closedBall_subset_ball le_of_tendsto instClosedIicTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal nhdsGT_neBot LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.Tendsto.div IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_const_nhds inf_le_left LT.lt.ne'
gauge_closure_zero 📖	mathematical	—	gauge SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real Real.normedField closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Pi.instZero Real.instZero	—	gauge_def' norm_smul NormedSpace.toNormSMulClass NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass LE.le.eq_or_lt' norm_nonneg Set.ext csInf_Ioi instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Set.eq_empty_of_forall_notMem LT.lt.ne' Membership.mem.out Real.sInf_empty
gauge_def 📖	mathematical	—	gauge InfSet.sInf Real Real.instInfSet setOf Set Set.instMembership Set.Ioi Real.instPreorder Real.instZero Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid	—	—
gauge_def' 📖	mathematical	—	gauge InfSet.sInf Real Real.instInfSet setOf Set Set.instMembership Set.Ioi Real.instPreorder Real.instZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid Real.instInv	—	Set.mem_smul_set_iff_inv_smul_mem₀ LT.lt.ne'
gauge_empty 📖	mathematical	—	gauge Set Set.instEmptyCollection Pi.instZero Real Real.instZero	—	gauge_def' Set.sep_false Real.sInf_empty
gauge_eq_one_iff_mem_frontier 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	gauge Real.instOne Set.instMembership frontier	—	eq_iff_le_not_lt gauge_le_one_iff_mem_closure gauge_lt_one_iff_mem_interior
gauge_eq_zero 📖	mathematical	Absorbent Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	gauge Real.instZero	—	by_contra comap_gauge_nhds_zero_le IsOpen.mem_nhds isOpen_compl_singleton Filter.HasBasis.mem_iff Filter.HasBasis.comap nhds_basis_zero_abs_lt Real.instIsOrderedAddMonoid instOrderTopologyReal instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial abs_zero IsOrderedAddMonoid.toAddLeftMono gauge_zero
gauge_le_eq 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Absorbent PseudoMetricSpace.toBornology Real.pseudoMetricSpace Real.instLE Real.instZero	setOf gauge Set.iInter Real.instLT Set.smulSet	—	Set.ext LE.le.trans_lt Set.mem_smul_set_iff_inv_smul_mem₀ LT.lt.ne' exists_lt_of_gauge_lt Convex.smul_mem_of_zero_mem covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_of_lt mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE inv_mul_le_iff₀ mul_one LT.lt.le mul_inv_cancel_right₀ smul_smul le_of_forall_pos_lt_add lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike CancelDenoms.sub_subst CancelDenoms.add_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.isNat_mul gauge_le_of_mem le_of_not_gt Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.mul_neg
gauge_le_of_mem 📖	mathematical	Real Real.instLE Real.instZero Set Set.instMembership Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid	gauge	—	LE.le.eq_or_lt Set.mem_singleton_iff Set.zero_smul_set_subset gauge_zero le_refl csInf_le
gauge_le_one_iff_mem_closure 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Real.instLE gauge Real.instOne Set.instMembership closure	—	mem_closure_of_gauge_le_one mem_of_mem_nhds absorbent_nhds_zero le_on_closure OrderTopology.to_orderClosedTopology instOrderTopologyReal gauge_le_one_of_mem Continuous.continuousOn continuous_gauge continuousOn_const
gauge_le_one_of_mem 📖	mathematical	Set Set.instMembership	Real Real.instLE gauge Real.instOne	—	gauge_le_of_mem zero_le_one Real.instZeroLEOneClass one_smul
gauge_lt_eq 📖	mathematical	Absorbent Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid	setOf Real.instLT gauge Set.iUnion Set Set.instMembership Set.Ioo Real.instPreorder Real.instZero Set.smulSet	—	Set.ext exists_lt_of_gauge_lt LE.le.trans_lt gauge_le_of_mem LT.lt.le
gauge_lt_eq' 📖	mathematical	Absorbent Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid	setOf Real.instLT gauge Set.iUnion Real.instZero Set Set.smulSet	—	Set.ext exists_lt_of_gauge_lt LE.le.trans_lt gauge_le_of_mem LT.lt.le
gauge_lt_of_mem_smul 📖	mathematical	Real Real.instLT Real.instZero IsOpen Set Set.instMembership Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid	gauge	—	Set.mem_smul_set_iff_inv_smul_mem₀ LT.lt.ne' gauge_lt_one_of_mem_of_isOpen mul_one inv_mul_lt_iff₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing smul_eq_mul gauge_smul_of_nonneg IsStrictOrderedRing.toIsStrictOrderedModule Set.isScalarTower IsScalarTower.left inv_nonneg LT.lt.le
gauge_lt_one_eq_interior 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	setOf Real.instLT gauge Real.instOne interior	—	Set.Subset.antisymm mem_openSegment_of_gauge_lt_one absorbent_nhds_zero Convex.openSegment_interior_self_subset_interior ContinuousSMul.continuousConstSMul mem_interior_iff_mem_nhds interior_subset_gauge_lt_one
gauge_lt_one_eq_self_of_isOpen 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid IsOpen	setOf Real.instLT gauge Real.instOne	—	HasSubset.Subset.antisymm Set.instAntisymmSubset gauge_lt_one_subset_self absorbent_nhds_zero IsOpen.mem_nhds IsOpen.interior_eq interior_subset_gauge_lt_one
gauge_lt_one_iff_mem_interior 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Real.instLT gauge Real.instOne Set.instMembership interior	—	Set.ext_iff gauge_lt_one_eq_interior
gauge_lt_one_of_mem_of_isOpen 📖	mathematical	IsOpen Set Set.instMembership	Real Real.instLT gauge Real.instOne	—	interior_subset_gauge_lt_one IsOpen.interior_eq
gauge_lt_one_subset_self 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Absorbent PseudoMetricSpace.toBornology Real.pseudoMetricSpace	Set.instHasSubset setOf Real.instLT gauge Real.instOne	—	mem_openSegment_of_gauge_lt_one Convex.openSegment_subset
gauge_mono 📖	mathematical	Absorbent Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid Set Set.instHasSubset	Pi.hasLe Real.instLE gauge	—	csInf_le_csInf Absorbent.gauge_set_nonempty Set.setOf_subset_setOf_of_imp Mathlib.Tactic.GCongr.and_right_mono Set.mem_of_subset_of_mem Set.smul_set_mono
gauge_neg 📖	mathematical	Set Set.instMembership NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	gauge	—	neg_neg gauge_def' smul_neg
gauge_neg_set_eq_gauge_neg 📖	mathematical	—	gauge Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	gauge_neg_set_neg neg_neg
gauge_neg_set_neg 📖	mathematical	—	gauge Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	gauge_def' smul_neg
gauge_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero gauge	—	Real.sInf_nonneg LT.lt.le
gauge_norm_smul 📖	mathematical	Balanced SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	gauge Real Real.instMonoid Real.semiring Norm.norm NormedField.toNorm	—	RCLike.real_smul_eq_coe_smul Balanced.smul_mem_iff Balanced.smul IsScalarTower.to_smulCommClass' RCLike.norm_ofReal abs_norm
gauge_of_subset_zero 📖	mathematical	Set Set.instHasSubset Set.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	gauge Pi.instZero Real Real.instZero	—	Set.subset_singleton_iff_eq gauge_empty gauge_zero'
gauge_pos 📖	mathematical	Absorbent Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Real.instLT Real.instZero gauge	—	LE.le.lt_iff_ne' gauge_nonneg gauge_eq_zero
gauge_smul 📖	mathematical	Balanced SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	gauge Real Real.instMul Norm.norm NormedField.toNorm	—	smul_eq_mul gauge_smul_of_nonneg Real.instIsStrictOrderedRing IsStrictOrderedRing.toIsStrictOrderedModule Set.isScalarTower IsScalarTower.left norm_nonneg gauge_norm_smul
gauge_smul_left 📖	mathematical	Set Set.instMembership NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	gauge Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid Function.hasSMul Real Real.instZero SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass MulActionWithZero.toSMulWithZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	gauge_smul_left_of_nonneg abs_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing covariant_swap_add_of_covariant_add abs_choice Set.neg_smul_set Set.smul_set_neg Set.ext neg_neg
gauge_smul_left_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	gauge Set Set.smulSet SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulWithZero.toSMulZeroClass MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulActionWithZero.toSMulWithZero Function.hasSMul Real Real.instZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	LE.le.eq_or_lt inv_zero zero_smul gauge_of_subset_zero Set.zero_smul_set_subset gauge_def' Pi.smul_apply Real.sInf_smul_of_nonneg IsStrictOrderedModule.toIsOrderedModule inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Set.ext smul_pos IsStrictOrderedModule.toPosSMulStrictMono smul_inv₀ smul_assoc inv_smul_smul₀ LT.lt.ne' Set.mem_Ioi inv_pos inv_inv
gauge_smul_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	gauge SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulWithZero.toSMulZeroClass MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulActionWithZero.toSMulWithZero Real Real.instZero	—	LE.le.eq_or_lt zero_smul gauge_zero gauge_def' Real.sInf_smul_of_nonneg IsStrictOrderedModule.toIsOrderedModule Set.ext smul_pos IsStrictOrderedModule.toPosSMulStrictMono inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Set.mem_smul_set_iff_inv_smul_mem₀ LT.lt.ne' smul_assoc inv_ne_zero inv_inv smul_inv_smul₀ Set.mem_Ioi Set.smul_mem_smul_set
gauge_sum_le 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Absorbent PseudoMetricSpace.toBornology Real.pseudoMetricSpace	Real.instLE gauge Finset.sum Real.instAddCommMonoid	—	Finset.le_sum_of_subadditive Real.instIsOrderedAddMonoid Eq.le gauge_zero gauge_add_le
gauge_unit_ball 📖	mathematical	—	gauge SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real Real.normedField Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instOne Norm.norm SeminormedAddCommGroup.toNorm	—	ball_normSeminorm Seminorm.gauge_ball coe_normSeminorm
gauge_zero 📖	mathematical	—	gauge NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real Real.instZero	—	gauge_def' smul_zero Set.sep_true csInf_Ioi instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Set.sep_false Real.sInf_empty
gauge_zero' 📖	mathematical	—	gauge Set Set.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Pi.instZero Real Real.instZero	—	gauge_def' eq_or_ne smul_zero Set.sep_true csInf_Ioi instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero Set.eq_empty_iff_forall_notMem ne_of_gt Real.sInf_empty
interior_subset_gauge_lt_one 📖	mathematical	—	Set Set.instHasSubset interior setOf Real Real.instLT gauge Real.instOne	—	Filter.Tendsto.mono_left Filter.Tendsto.smul Filter.Tendsto.inv₀ IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal Filter.tendsto_id one_ne_zero NeZero.charZero_one RCLike.charZero_rclike tendsto_const_nhds inf_le_left Filter.mp_mem Ioo_mem_nhdsLT instClosedIicTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal one_pos Real.instZeroLEOneClass one_smul inv_one mem_interior_iff_mem_nhds Filter.univ_mem' Set.mem_smul_set_iff_inv_smul_mem₀ LT.lt.ne' Filter.Eventually.exists nhdsLT_neBot LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial LE.le.trans_lt gauge_le_of_mem LT.lt.le
le_gauge_of_notMem 📖	mathematical	StarConvex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Absorbs PseudoMetricSpace.toBornology Real.pseudoMetricSpace Set Set.instSingletonSet Set.instMembership Set.smulSet	Real.instLE gauge	—	Absorbs.exists_pos le_csInf Set.singleton_subset_iff Eq.ge Real.norm_of_nonneg LT.lt.le not_lt LT.lt.trans starConvex_zero_iff covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_of_lt mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE div_eq_inv_mul div_le_one_of_le₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instZeroLEOneClass SemigroupAction.mul_smul mul_inv_cancel_left₀ LT.lt.ne'
le_gauge_of_subset_closedBall 📖	mathematical	Absorbent Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Real.instLE Real.instZero Set Set.instHasSubset Metric.closedBall NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm NormedAddCommGroup.toNorm gauge	—	gauge_closedBall gauge_mono
mem_closure_of_gauge_le_one 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Absorbent PseudoMetricSpace.toBornology Real.pseudoMetricSpace Real.instLE gauge Real.instOne	closure	—	Filter.mp_mem Ico_mem_nhdsLT instClosedIicTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal one_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Filter.univ_mem' gauge_lt_one_subset_self Set.mem_setOf_eq gauge_smul_of_nonneg Real.instIsStrictOrderedRing IsStrictOrderedRing.toIsStrictOrderedModule Set.isScalarTower IsScalarTower.left mul_lt_one_of_nonneg_of_lt_one_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing mem_closure_of_tendsto nhdsLT_neBot LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial Real.instNontrivial Filter.Tendsto.mono_left Continuous.tendsto' Continuous.smul continuous_id' continuous_const one_smul inf_le_left
mem_frontier_of_gauge_eq_one 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Absorbent PseudoMetricSpace.toBornology Real.pseudoMetricSpace gauge Real.instOne	frontier	—	mem_closure_of_gauge_le_one Eq.le LT.lt.ne Membership.mem.out interior_subset_gauge_lt_one
mem_openSegment_of_gauge_lt_one 📖	mathematical	Absorbent Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid Real.instLT gauge Real.instOne	Set Set.instMembership openSegment Real.partialOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	exists_lt_of_gauge_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sub_add_cancel smul_zero zero_add
mul_gauge_le_norm 📖	mathematical	Set Set.instHasSubset Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	Real Real.instLE Real.instMul gauge NormedSpace.toModule Real.normedField Norm.norm SeminormedAddCommGroup.toNorm	—	le_or_gt LE.le.trans mul_nonpos_of_nonpos_of_nonneg IsOrderedRing.toMulPosMono Real.instIsOrderedRing gauge_nonneg norm_nonneg mul_comm le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing gauge_ball LT.lt.le gauge_mono absorbent_ball_zero
one_le_gauge_of_notMem 📖	mathematical	StarConvex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Absorbs PseudoMetricSpace.toBornology Real.pseudoMetricSpace Set Set.instSingletonSet Set.instMembership	Real.instLE Real.instOne gauge	—	le_gauge_of_notMem one_smul
self_subset_gauge_le_one 📖	mathematical	—	Set Set.instHasSubset setOf Real Real.instLE gauge Real.instOne	—	gauge_le_one_of_mem
tendsto_gauge_nhds_zero 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Filter.Tendsto Real gauge UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	Filter.Tendsto.mono_right tendsto_gauge_nhds_zero_nhdsGE inf_le_left
tendsto_gauge_nhds_zero_nhdsGE 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Filter.Tendsto Real gauge nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ici Real.instPreorder	—	Filter.HasBasis.tendsto_right_iff nhdsGE_basis_Icc instOrderTopologyReal instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Filter.mp_mem set_smul_mem_nhds_zero_iff ContinuousSMul.continuousConstSMul LT.lt.ne' Filter.univ_mem' gauge_nonneg gauge_le_of_mem LT.lt.le

---

← Back to Index