SeparationQuotient

📁 Source: Mathlib/Analysis/Normed/Group/SeparationQuotient.lean

Statistics

Metric	Count
Definitions SeparationQuotient, liftNormedAddGroupHom, liftNormedAddGroupHomEquiv, normedMk	4
Theorems apply_eq_apply_of_inseparable, liftNormedAddGroupHomEquiv_apply, liftNormedAddGroupHomEquiv_symm_apply_coe, liftNormedAddGroupHom_apply, liftNormedAddGroupHom_normNoninc, liftNormedAddGroupHom_norm_le, norm_liftNormedAddGroupHom_apply_le, norm_liftNormedAddGroupHom_le, norm_normedMk_eq_one, norm_normedMk_le, normedMk_apply, normedMk_eq_zero_iff	12
Total	16

SeparationQuotient

Definitions

Name	Category	Theorems
liftNormedAddGroupHom 📖	CompOp	6 math math: liftNormedAddGroupHom_normNoninc, norm_liftNormedAddGroupHom_apply_le, liftNormedAddGroupHomEquiv_apply, norm_liftNormedAddGroupHom_le, liftNormedAddGroupHom_apply, liftNormedAddGroupHom_norm_le
liftNormedAddGroupHomEquiv 📖	CompOp	2 math math: liftNormedAddGroupHomEquiv_apply, liftNormedAddGroupHomEquiv_symm_apply_coe
normedMk 📖	CompOp	5 math math: norm_normedMk_eq_one, norm_normedMk_le, normedMk_eq_zero_iff, normedMk_apply, liftNormedAddGroupHomEquiv_symm_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_apply_of_inseparable 📖	—	DFunLike.coe NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Inseparable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	—	eq_of_sub_eq_zero map_sub dist_eq_norm Metric.inseparable_iff
liftNormedAddGroupHomEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv NormedAddGroupHom SeparationQuotient UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup EquivLike.toFunLike Equiv.instEquivLike liftNormedAddGroupHomEquiv liftNormedAddGroupHom	—	—
liftNormedAddGroupHomEquiv_symm_apply_coe 📖	mathematical	—	NormedAddGroupHom DFunLike.coe Equiv SeparationQuotient UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup EquivLike.toFunLike Equiv.instEquivLike Equiv.symm liftNormedAddGroupHomEquiv NormedAddGroupHom.comp normedMk	—	—
liftNormedAddGroupHom_apply 📖	mathematical	DFunLike.coe NormedAddGroupHom NormedAddGroupHom.funLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	SeparationQuotient UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup liftNormedAddGroupHom ContinuousAddMonoidHom instAddMonoid AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid instTopologicalSpaceSeparationQuotient ContinuousAddMonoidHom.instFunLike liftContinuousAddMonoidHom ContinuousAddMonoidHom.toContinuousAddMonoidHom SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddGroupHom.toAddMonoidHomClass NormedAddGroupHom.instContinuousMapClass	—	—
liftNormedAddGroupHom_normNoninc 📖	mathematical	DFunLike.coe NormedAddGroupHom NormedAddGroupHom.funLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddGroupHom.NormNoninc	SeparationQuotient UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup liftNormedAddGroupHom	—	NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one le_trans norm_liftNormedAddGroupHom_apply_le mul_le_of_le_one_left IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg
liftNormedAddGroupHom_norm_le 📖	mathematical	DFunLike.coe NormedAddGroupHom NormedAddGroupHom.funLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real Real.instLE Norm.norm NormedAddGroupHom.hasOpNorm NNReal.toReal	SeparationQuotient UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup liftNormedAddGroupHom	—	LE.le.trans norm_liftNormedAddGroupHom_le
norm_liftNormedAddGroupHom_apply_le 📖	mathematical	DFunLike.coe NormedAddGroupHom NormedAddGroupHom.funLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm SeparationQuotient UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup liftNormedAddGroupHom Real.instMul NormedAddGroupHom.hasOpNorm instNorm	—	NormedAddGroupHom.le_opNorm
norm_liftNormedAddGroupHom_le 📖	mathematical	DFunLike.coe NormedAddGroupHom NormedAddGroupHom.funLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	Real Real.instLE Norm.norm SeparationQuotient UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup NormedAddGroupHom.hasOpNorm liftNormedAddGroupHom	—	NormedAddGroupHom.opNorm_le_bound norm_nonneg norm_liftNormedAddGroupHom_apply_le
norm_normedMk_eq_one 📖	mathematical	—	Norm.norm NormedAddGroupHom SeparationQuotient UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup NormedAddGroupHom.hasOpNorm normedMk Real Real.instOne	—	NormedAddGroupHom.opNorm_eq_of_bounds zero_le_one Real.instZeroLEOneClass one_mul le_rfl exists_norm_ne_zero one_le_of_le_mul_right₀ MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing lt_of_le_of_ne' norm_nonneg
norm_normedMk_le 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddGroupHom SeparationQuotient UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup NormedAddGroupHom.hasOpNorm normedMk Real.instOne	—	NormedAddGroupHom.opNorm_le_bound zero_le_one Real.instZeroLEOneClass one_mul
normedMk_apply 📖	mathematical	—	DFunLike.coe NormedAddGroupHom SeparationQuotient UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup NormedAddGroupHom.funLike normedMk ZeroHom.toFun AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup instAddZeroClass AddMonoidHom.toZeroHom mkAddMonoidHom	—	—
normedMk_eq_zero_iff 📖	mathematical	—	normedMk NormedAddGroupHom SeparationQuotient UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroup NormedAddGroupHom.zero Norm.norm SeminormedAddCommGroup.toNorm Real Real.instZero	—	mk_eq_zero_iff NormedAddGroupHom.ext norm_norm

(root)

Definitions

Name	Category	Theorems
SeparationQuotient 📖	CompOp	152 math math: SeparationQuotient.t2Space, SeparationQuotient.instNormOneClass, SeparationQuotient.liftNormedAddGroupHom_normNoninc, SeparationQuotient.lift_comp_mk, SeparationQuotient.mkCLM_comp_outCLM, SeparationQuotient.tendsto_lift_nhds_mk, SeparationQuotient.continuous_mk, SeparationQuotient.instNormalSpace, SeparationQuotient.map_mk_nhdsSet, SeparationQuotient.isQuotientMap_prodMap_mk, SeparationQuotient.instContinuousNeg, SeparationQuotient.norm_liftNormedAddGroupHom_apply_le, SeparationQuotient.instIsTopologicalGroup, SeparationQuotient.uniformity_eq, SeparationQuotient.instIsPretransitiveVAdd, SeparationQuotient.comap_mk_nhds_mk, SeparationQuotient.mkAddMonoidHom_apply, SeparationQuotient.mk_zsmul, SeparationQuotient.tendsto_lift₂_nhds, SeparationQuotient.uniformContinuous_mk, SeparationQuotient.nnnorm_mk', SeparationQuotient.instContinuousInv, SeparationQuotient.continuousAt_lift, SeparationQuotient.preimage_image_mk_closed, SeparationQuotient.isInducing_mk, SeparationQuotient.continuous_lift, SeparationQuotient.instIsUniformGroup, SeparationQuotient.liftNormedAddGroupHomEquiv_apply, SeparationQuotient.instT0Space, SeparationQuotient.mk_smul, SeparationQuotient.tendsto_lift₂_nhdsWithin, SeparationQuotient.mk_one, SeparationQuotient.norm_normedMk_eq_one, SeparationQuotient.norm_normedMk_le, SeparationQuotient.isUniformInducing_mk, instT3SpaceSeparationQuotientOfRegularSpace, SeparationQuotient.outCLM_uniformContinuous, SeparationQuotient.mk_div, SeparationQuotient.uniformContinuous_lift, SeparationQuotient.range_mk, SeparationQuotient.instNonempty, SeparationQuotient.uniformContinuous_lift', SeparationQuotient.mk_intCast, SeparationQuotient.instIsScalarTower, SeparationQuotient.continuousWithinAt_lift, UniformSpace.topologicalRing, SeparationQuotient.instSubsingletonOfIndiscreteTopology, SeparationQuotient.map_id, SeparationQuotient.mk_neg, SeparationQuotient.uniformContinuous_dom₂, SeparationQuotient.outCLM_isUniformEmbedding, instIsBoundedSMulSeparationQuotient, SeparationQuotient.completeSpace_iff, SeparationQuotient.isQuotientMap_mk, SeparationQuotient.mk_zpow, SeparationQuotient.image_mk_closure, SeparationQuotient.mk_mul, SeparationQuotient.mk_add, SeparationQuotient.continuousOn_lift, SeparationQuotient.edist_mk, SeparationQuotient.instIsCentralVAdd, SeparationQuotient.mk_inv, SeparationQuotient.t1Space_iff, SeparationQuotient.normedMk_eq_zero_iff, SeparationQuotient.mk_eq_zero_iff, SeparationQuotient.exists_out_continuousLinearMap, SeparationQuotient.mk_pow, SeparationQuotient.instIsCentralScalar, SeparationQuotient.mk_sub, SeparationQuotient.instNontrivialOfNontrivialTopology, SeparationQuotient.mk_outCLM, SeparationQuotient.instContinuousAdd, SeparationQuotient.continuousAt_lift₂, SeparationQuotient.isOpenMap_mk, CauchyFilter.separated_pureCauchy_injective, UniformSpace.Completion.coe_eq, SeparationQuotient.instIsUniformAddGroup, SeparationQuotient.norm_liftNormedAddGroupHom_le, SeparationQuotient.nontrivial_iff, SeparationQuotient.mk_nsmul, SeparationQuotient.uniformContinuous_uncurry_lift₂, SeparationQuotient.instIsPretransitiveSMul, SeparationQuotient.postcomp_mkCLM_surjective, SeparationQuotient.inner_mk_mk, SeparationQuotient.instContinuousDiv, IsUltraUniformity.separationQuotient_iff, SeparationQuotient.mk_comp_outCLM, SeparationQuotient.norm_mk', IsUltraUniformity.separationQuotient, SeparationQuotient.mk_natCast, SeparationQuotient.mk_algebraMap, UniformSpace.Completion.uniformContinuous_completionSeparationQuotientEquiv_symm, SeparationQuotient.surjective_mk, SeparationQuotient.liftContinuousAddCommMonoidHom_mk, SeparationQuotient.preimage_mk_closure, SeparationQuotient.nnnorm_mk, SeparationQuotient.mkMonoidHom_apply, instT5SpaceSeparationQuotientOfCompletelyNormalSpaceOfR0Space, SeparationQuotient.instContinuousConstSMul, SeparationQuotient.liftCLM_apply, SeparationQuotient.isOpenQuotientMap_mk, SeparationQuotient.preimage_mk_interior, SeparationQuotient.normedMk_apply, SeparationQuotient.comap_mk_uniformity, SeparationQuotient.uniformContinuous_map, SeparationQuotient.mk_ofNat, SeparationQuotient.mkRingHom_apply, SeparationQuotient.liftNormedAddGroupHom_apply, SeparationQuotient.comap_map_mk_uniformity, SeparationQuotient.mk_vadd, SeparationQuotient.instSMulCommClass, SeparationQuotient.mk_eq_one_iff, SeparationQuotient.preimage_mk_frontier, SeparationQuotient.instCompleteSpace, SeparationQuotient.comap_mk_nhdsSet_image, SeparationQuotient.instContinuousMul, SeparationQuotient.comap_mk_nhdsSet, SeparationQuotient.continuousWithinAt_lift₂, SeparationQuotient.isEmbedding_outCLM, SeparationQuotient.tendsto_lift_nhdsWithin_mk, SeparationQuotient.norm_mk, SeparationQuotient.map_mk_nhdsWithin_preimage, SeparationQuotient.liftCLM_mk, SeparationQuotient.dist_mk, SeparationQuotient.map_comp, SeparationQuotient.t2Space_iff, SeparationQuotient.continuousOn_lift₂, UniformSpace.Completion.uniformContinuous_completionSeparationQuotientEquiv, SeparationQuotient.continuous_lift₂, SeparationQuotient.instVAddCommClass, SeparationQuotient.instSubsingleton, SeparationQuotient.preimage_image_mk_open, SeparationQuotient.subsingleton_iff, SeparationQuotient.map_prod_map_mk_nhds, SeparationQuotient.instContinuousSMul, SeparationQuotient.instRightDistribClass, SeparationQuotient.mkCLM_apply, SeparationQuotient.liftContinuousCommMonoidHom_mk, SeparationQuotient.instVAddAssocClass, SeparationQuotient.isClosedMap_mk, SeparationQuotient.map_mk_nhds, SeparationQuotient.liftNormedAddGroupHomEquiv_symm_apply_coe, SeparationQuotient.instModuleFinite, SeparationQuotient.instContinuousSub, SeparationQuotient.outCLM_injective, SeparationQuotient.mk_zero, SeparationQuotient.uniformContinuous_dom, SeparationQuotient.instLeftDistribClass, SeparationQuotient.liftNormedAddGroupHom_norm_le, SeparationQuotient.instIsTopologicalAddGroup, SeparationQuotient.instContinuousConstVAdd, SeparationQuotient.outCLM_isUniformInducing

---

← Back to Index