Continuous

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

Statistics

Metric	Count
Definitions	0
Theorems continuousOn, continuousOn_interior, continuousOn_tfae, exists_lipschitzOnWith_of_isBounded, isBoundedUnder_abs, lipschitzOnWith_of_abs_le, locallyLipschitz, locallyLipschitzOn, locallyLipschitzOn_iff_continuousOn, locallyLipschitzOn_interior, continuousOn, continuousOn_interior, continuousOn_tfae, exists_lipschitzOnWith_of_isBounded, isBoundedUnder_abs, lipschitzOnWith_of_abs_le, locallyLipschitz, locallyLipschitzOn, locallyLipschitzOn_iff_continuousOn, locallyLipschitzOn_interior	20
Total	20

ConcaveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ConcaveOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	ContinuousOn Real.pseudoMetricSpace	—	LocallyLipschitzOn.continuousOn locallyLipschitzOn
continuousOn_interior 📖	mathematical	ConcaveOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	ContinuousOn Real.pseudoMetricSpace interior	—	LocallyLipschitzOn.continuousOn locallyLipschitzOn_interior
continuousOn_tfae 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.Nonempty ConcaveOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	List.TFAE LocallyLipschitzOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real.metricSpace ContinuousOn Real.pseudoMetricSpace Set Set.instMembership ContinuousAt Filter.IsBoundedUnder Real.instLE nhds	—	ConvexOn.continuousOn_tfae neg Real.instIsOrderedAddMonoid Equiv.exists_congr IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal abs_neg
exists_lipschitzOnWith_of_isBounded 📖	mathematical	ConcaveOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Metric.ball Real.instLT Bornology.IsBounded PseudoMetricSpace.toBornology Real.pseudoMetricSpace Set.image	LipschitzOnWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real.metricSpace	—	Set.ext Set.image_congr Bornology.IsBounded.neg ConvexOn.exists_lipschitzOnWith_of_isBounded neg Real.instIsOrderedAddMonoid
isBoundedUnder_abs 📖	mathematical	ConcaveOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set Filter Filter.instMembership nhds	Filter.IsBoundedUnder Real.instLE abs Pi.instLattice Real.lattice Pi.addGroup Real.instAddGroup	—	abs_neg Real.instIsOrderedAddMonoid ConvexOn.isBoundedUnder_abs neg
lipschitzOnWith_of_abs_le 📖	mathematical	ConcaveOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Metric.ball Real.instLT Real.instZero Real.instLE abs Real.lattice Real.instAddGroup	LipschitzOnWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real.metricSpace Real.toNNReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub	—	Nat.instAtLeastTwoHAddOfNat ConvexOn.lipschitzOnWith_of_abs_le neg Real.instIsOrderedAddMonoid abs_neg
locallyLipschitz 📖	mathematical	ConcaveOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.univ	LocallyLipschitz EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real.metricSpace	—	interior_univ locallyLipschitzOn_interior
locallyLipschitzOn 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ConcaveOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	LocallyLipschitzOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real.metricSpace	—	ConvexOn.locallyLipschitzOn neg Real.instIsOrderedAddMonoid
locallyLipschitzOn_iff_continuousOn 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ConcaveOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	LocallyLipschitzOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real.metricSpace ContinuousOn Real.pseudoMetricSpace	—	IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal ConvexOn.locallyLipschitzOn_iff_continuousOn neg Real.instIsOrderedAddMonoid
locallyLipschitzOn_interior 📖	mathematical	ConcaveOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	LocallyLipschitzOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real.metricSpace interior	—	locallyLipschitzOn isOpen_interior subset interior_subset Convex.interior SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Real.instZeroLEOneClass

ConvexOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ConvexOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	ContinuousOn Real.pseudoMetricSpace	—	LocallyLipschitzOn.continuousOn locallyLipschitzOn
continuousOn_interior 📖	mathematical	ConvexOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	ContinuousOn Real.pseudoMetricSpace interior	—	LocallyLipschitzOn.continuousOn locallyLipschitzOn_interior
continuousOn_tfae 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.Nonempty ConvexOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	List.TFAE LocallyLipschitzOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real.metricSpace ContinuousOn Real.pseudoMetricSpace Set Set.instMembership ContinuousAt Filter.IsBoundedUnder Real.instLE nhds	—	LocallyLipschitzOn.continuousOn ContinuousOn.continuousAt IsOpen.mem_nhds Filter.Tendsto.eventually eventually_le_nhds instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono contravariant_lt_of_covariant_le Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike ContinuousAt.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousAt.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousAt.inv₀ IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal instIsTopologicalAddGroupReal continuousAt_const continuousAt_id' Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Nat.cast_zero ContinuousAt.div₀ IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal sub_zero inv_one one_smul div_one zero_smul Filter.Eventually.exists_gt nhdsGT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.Eventually.and eventually_lt_nhds zero_lt_one Metric.eventually_nhds_iff IsOpen.eventually_mem mul_pos MulAction.injective₀ sub_ne_zero LT.lt.ne' div_eq_mul_inv smul_sub smul_smul inv_mul_cancel_left₀ smul_add sub_mul one_mul mul_inv_cancel₀ sub_smul mul_left_comm mul_one sub_sub_sub_cancel_left sub_add_sub_cancel smul_inv_smul₀ add_add_sub_cancel sub_add_cancel dist_add_right NormedAddGroup.to_isIsometricVAdd_right dist_smul₀ NormedSpace.toNormSMulClass norm_inv abs_of_nonneg LT.lt.le dist_sub_eq_dist_add_right le_max_of_mem_segment IsStrictOrderedRing.toIsStrictOrderedModule sub_nonneg covariant_swap_add_of_covariant_add add_sub_cancel sup_le_sup le_refl isBoundedUnder_abs Metric.mem_nhds_iff Filter.inter_mem IsOpen.nhdsWithin_eq Nat.instAtLeastTwoHAddOfNat exists_lipschitzOnWith_of_isBounded subset convex_ball half_lt_self isBounded_iff_forall_norm_le Metric.ball_mem_nhds List.tfae_of_cycle
exists_lipschitzOnWith_of_isBounded 📖	mathematical	ConvexOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Metric.ball Real.instLT Bornology.IsBounded PseudoMetricSpace.toBornology Real.pseudoMetricSpace Set.image	LipschitzOnWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real.metricSpace	—	dist_zero_right Metric.isBounded_iff_subset_ball sub_sub_cancel Nat.instAtLeastTwoHAddOfNat lipschitzOnWith_of_abs_le sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le
isBoundedUnder_abs 📖	mathematical	ConvexOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set Filter Filter.instMembership nhds	Filter.IsBoundedUnder Real.instLE abs Pi.instLattice Real.lattice Pi.addGroup Real.instAddGroup	—	Filter.IsBoundedUnder.mono_le Filter.Eventually.of_forall le_abs_self Nat.instAtLeastTwoHAddOfNat Metric.tendsto_nhds_nhds dist_comm two_nsmul dist_sub_eq_dist_add_right dist_add_left NormedAddGroup.to_isIsometricVAdd_left Filter.mp_mem Filter.Tendsto.eventually Filter.Tendsto.eventually_mem Filter.univ_mem' LE.le.trans IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instIsOrderedRing Real.instNontrivial covariant_swap_add_of_covariant_add sub_le_iff_le_add neg_sub_comm sub_le_iff_le_add' abs_two abs_mul neg_abs_le le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo add_halves CharZero.NeZero.two RCLike.charZero_rclike Nat.cast_smul_eq_nsmul Nat.cast_two Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos one_mul CancelDenoms.cancel_factors_le CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_mul CancelDenoms.add_subst CancelDenoms.mul_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_lt_true Nat.cast_zero one_div smul_sub inv_smul_smul₀ add_sub_cancel add_le_add_right
lipschitzOnWith_of_abs_le 📖	mathematical	ConvexOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Metric.ball Real.instLT Real.instZero Real.instLE abs Real.lattice Real.instAddGroup	LipschitzOnWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real.metricSpace Real.toNNReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub	—	Nat.instAtLeastTwoHAddOfNat eq_or_ne sub_self norm_zero MulZeroClass.mul_zero Metric.ball_subset_ball le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl 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.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing norm_sub_pos_iff mem_ball_iff_norm add_sub_right_comm norm_add_le add_lt_add_of_lt_of_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add norm_smul NormedSpace.toNormSMulClass norm_div abs_of_nonneg LT.lt.le norm_norm IsUnit.div_mul_cancel LT.lt.ne' sub_add_cancel Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt add_pos' Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_ne_zero NeZero.one GroupWithZero.toNontrivial Convex.combo_self smul_sub smul_add smul_smul div_mul_div_cancel₀' Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.const_add_termg Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg mul_comm mul_div_assoc le_div_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono le_of_lt div_pos Mathlib.Tactic.LinearCombination.le_of_le Real.instIsOrderedCancelAddMonoid Mathlib.Tactic.FieldSimp.le_eq_cancel_le PosMulStrictMono.toPosMulMono Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.cons_pos Real.instZeroLEOneClass zero_lt_one Mathlib.Tactic.LinearCombination.le_rearrange Mathlib.Tactic.Ring.le_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul le_refl sub_eq_add_neg two_mul mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono add_le_add LE.le.trans le_abs_self neg_le_abs LipschitzOnWith.of_dist_le' dist_eq_norm_sub norm_sub_rev
locallyLipschitz 📖	mathematical	ConvexOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.univ	LocallyLipschitz EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real.metricSpace	—	interior_univ locallyLipschitzOn_interior
locallyLipschitzOn 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ConvexOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	LocallyLipschitzOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real.metricSpace	—	Set.eq_empty_or_nonempty exists_mem_interior_convexHull_affineBasis IsOpen.mem_nhds List.TFAE.out continuousOn_tfae BddAbove.isBoundedUnder isOpen_interior BddAbove.mono Set.image_mono interior_subset bddAbove_convexHull Real.instIsStrictOrderedRing Real.instIsOrderedAddMonoid IsStrictOrderedRing.toIsStrictOrderedModule HasSubset.Subset.trans Set.instIsTransSubset subset_convexHull Set.Finite.bddAbove instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean Set.Finite.image Set.finite_range Finite.of_fintype
locallyLipschitzOn_iff_continuousOn 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ConvexOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	LocallyLipschitzOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real.metricSpace ContinuousOn Real.pseudoMetricSpace	—	Set.eq_empty_or_nonempty List.TFAE.out continuousOn_tfae
locallyLipschitzOn_interior 📖	mathematical	ConvexOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	LocallyLipschitzOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real.metricSpace interior	—	locallyLipschitzOn isOpen_interior subset interior_subset Convex.interior SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Real.instZeroLEOneClass

---

← Back to Index