GaugeRescale

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

Statistics

Metric	Count
Definitions gaugeRescale, gaugeRescaleEquiv, gaugeRescaleHomeomorph	3
Theorems continuous_gaugeRescale, exists_homeomorph_image_eq, exists_homeomorph_image_interior_closure_frontier_eq_unitBall, gaugeRescale_def, gaugeRescale_gaugeRescale, gaugeRescale_self, gaugeRescale_self_apply, gaugeRescale_smul, gaugeRescale_zero, gauge_gaugeRescale, gauge_gaugeRescale', gauge_gaugeRescale_le, image_gaugeRescaleHomeomorph_closure, image_gaugeRescaleHomeomorph_interior, mapsTo_gaugeRescale_closure, mapsTo_gaugeRescale_interior	16
Total	19

(root)

Definitions

Name	Category	Theorems
gaugeRescale 📖	CompOp	12 math math: gaugeRescale_self_apply, gauge_gaugeRescale, mapsTo_gaugeRescale_closure, continuous_gaugeRescale, gaugeRescale_zero, gauge_gaugeRescale', mapsTo_gaugeRescale_interior, gaugeRescale_gaugeRescale, gaugeRescale_self, gaugeRescale_def, gauge_gaugeRescale_le, gaugeRescale_smul
gaugeRescaleEquiv 📖	CompOp	—
gaugeRescaleHomeomorph 📖	CompOp	2 math math: image_gaugeRescaleHomeomorph_interior, image_gaugeRescaleHomeomorph_closure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_gaugeRescale 📖	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 Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Continuous gaugeRescale	—	absorbent_nhds_zero continuous_iff_continuousAt eq_or_ne ContinuousAt.eq_1 gaugeRescale_zero comap_gauge_nhds_zero gauge_gaugeRescale tendsto_gauge_nhds_zero ContinuousAt.smul ContinuousAt.div IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuousAt_gauge LT.lt.ne' gauge_pos continuousAt_id
exists_homeomorph_image_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.Nonempty interior Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Set.image DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike closure frontier	—	interior_vadd VAddCommClass.continuousConstVAdd vaddCommClass_self IsTopologicalAddGroup.toContinuousAdd neg_neg add_zero Set.image_image Set.image_congr image_gaugeRescaleHomeomorph_interior vadd_neg_vadd closure_vadd image_gaugeRescaleHomeomorph_closure Set.image_diff Homeomorph.injective
exists_homeomorph_image_interior_closure_frontier_eq_unitBall 📖	mathematical	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Set.Nonempty interior Bornology.IsBounded PseudoMetricSpace.toBornology	Set.image DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Metric.ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne closure Metric.closedBall frontier Metric.sphere	—	IsOpen.interior_eq Metric.isOpen_ball closure_ball NeZero.charZero_one RCLike.charZero_rclike frontier_ball exists_homeomorph_image_eq SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace NormedSpace.isVonNBounded_of_isBounded convex_ball Real.instZeroLEOneClass NormedSpace.isVonNBounded_ball
gaugeRescale_def 📖	mathematical	—	gaugeRescale Real 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 DivInvMonoid.toDiv Real.instDivInvMonoid gauge	—	—
gaugeRescale_gaugeRescale 📖	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	gaugeRescale	—	eq_or_ne gaugeRescale_zero gaugeRescale_def gaugeRescale_smul div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing gauge_nonneg gaugeRescale.eq_1 smul_smul div_mul_div_cancel₀ LT.lt.ne' gauge_pos
gaugeRescale_self 📖	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	gaugeRescale	—	gaugeRescale_self_apply
gaugeRescale_self_apply 📖	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	gaugeRescale	—	eq_or_ne gaugeRescale_zero gaugeRescale.eq_1 div_self LT.lt.ne' gauge_pos one_smul
gaugeRescale_smul 📖	mathematical	Real Real.instLE Real.instZero	gaugeRescale 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_smul_of_nonneg Real.instIsStrictOrderedRing IsStrictOrderedRing.toIsStrictOrderedModule Set.isScalarTower IsScalarTower.left smul_smul mul_div_mul_comm mul_right_comm div_self_mul_self
gaugeRescale_zero 📖	mathematical	—	gaugeRescale NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	smul_zero
gauge_gaugeRescale 📖	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 gaugeRescale	—	eq_or_ne gaugeRescale_zero gauge_zero gauge_gaugeRescale' LT.lt.ne' gauge_pos
gauge_gaugeRescale' 📖	mathematical	—	gauge gaugeRescale	—	gaugeRescale.eq_1 gauge_smul_of_nonneg Real.instIsStrictOrderedRing IsStrictOrderedRing.toIsStrictOrderedModule Set.isScalarTower IsScalarTower.left div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono gauge_nonneg smul_eq_mul div_mul_cancel₀
gauge_gaugeRescale_le 📖	mathematical	—	Real Real.instLE gauge gaugeRescale	—	div_zero zero_smul gauge_zero Eq.le gauge_gaugeRescale'
image_gaugeRescaleHomeomorph_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 Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Set.image DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike gaugeRescaleHomeomorph closure	—	Set.Subset.antisymm Set.MapsTo.image_subset mapsTo_gaugeRescale_closure mem_of_mem_nhds absorbent_nhds_zero Homeomorph.preimage_symm Set.image_subset_iff
image_gaugeRescaleHomeomorph_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 Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Set.image DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike gaugeRescaleHomeomorph interior	—	Set.Subset.antisymm Set.MapsTo.image_subset mapsTo_gaugeRescale_interior Homeomorph.preimage_symm Set.image_subset_iff
mapsTo_gaugeRescale_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 Set.instMembership Absorbent PseudoMetricSpace.toBornology Real.pseudoMetricSpace	Set.MapsTo gaugeRescale closure	—	mem_closure_of_gauge_le_one LE.le.trans gauge_gaugeRescale_le gauge_le_one_iff_mem_closure
mapsTo_gaugeRescale_interior 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid 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.MapsTo gaugeRescale interior	—	gauge_lt_one_iff_mem_interior LE.le.trans_lt gauge_gaugeRescale_le interior_subset_gauge_lt_one

---

← Back to Index