Section

📁 Source: Mathlib/Topology/Algebra/SeparationQuotient/Section.lean

Statistics

Metric	Count
Definitions Section, Section, outCLM	3
Theorems exists_out_continuousLinearMap, isEmbedding_outCLM, mkCLM_comp_outCLM, mk_comp_outCLM, mk_outCLM, outCLM_injective, outCLM_isUniformEmbedding, outCLM_isUniformInducing, outCLM_uniformContinuous, postcomp_mkCLM_surjective	10
Total	13

AddGroupExtension

Definitions

Name	Category	Theorems
Section 📖	CompData	12 math math: Section.exists_eq_inl_add, Section.exists_add_eq_inl_add_add, Section.add_add_add_neg_mem_range_inl, Section.rightHom_comp_section, Section.rightHom_section, Section.exists_add_eq_add_add_inl, Section.equivComp_apply, Section.add_neg_mem_range_inl, Section.neg_add_mem_range_inl, Section.add_neg_add_add_mem_range_inl, Section.coe_mk, Section.exists_eq_add_inl

GroupExtension

Definitions

Name	Category	Theorems
Section 📖	CompData	12 math math: Section.mul_inv_mem_range_inl, Section.mul_inv_mul_mul_mem_range_inl, Section.coe_mk, Section.exists_mul_eq_mul_mul_inl, Section.inv_mul_mem_range_inl, Section.exists_eq_inl_mul, Section.rightHom_section, Section.mul_mul_mul_inv_mem_range_inl, Section.exists_mul_eq_inl_mul_mul, Section.exists_eq_mul_inl, Section.rightHom_comp_section, Section.equivComp_apply

SeparationQuotient

Definitions

Name	Category	Theorems
outCLM 📖	CompOp	8 math math: mkCLM_comp_outCLM, outCLM_uniformContinuous, outCLM_isUniformEmbedding, mk_outCLM, mk_comp_outCLM, isEmbedding_outCLM, outCLM_injective, outCLM_isUniformInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_out_continuousLinearMap 📖	mathematical	—	ContinuousLinearMap.comp DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring SeparationQuotient instTopologicalSpaceSeparationQuotient instAddCommMonoid AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instModule RingHomCompTriple.ids mkCLM ContinuousLinearMap.id	—	IsTopologicalAddGroup.toContinuousAdd RingHomCompTriple.ids LinearMap.exists_rightInverse_of_surjective Module.Projective.of_free Module.Free.of_divisionRing RingHomSurjective.ids LinearMap.range_eq_top Topology.IsInducing.continuous_iff continuous_id DFunLike.ext'
isEmbedding_outCLM 📖	mathematical	—	Topology.IsEmbedding SeparationQuotient instTopologicalSpaceSeparationQuotient DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instModule ContinuousLinearMap.funLike outCLM	—	Function.LeftInverse.isEmbedding IsTopologicalAddGroup.toContinuousAdd mk_outCLM ContinuousMapClass.map_continuous ContinuousSemilinearMapClass.toContinuousMapClass ContinuousLinearMap.continuousSemilinearMapClass
mkCLM_comp_outCLM 📖	mathematical	—	ContinuousLinearMap.comp DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring SeparationQuotient instTopologicalSpaceSeparationQuotient instAddCommMonoid AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instModule RingHomCompTriple.ids mkCLM outCLM ContinuousLinearMap.id	—	IsTopologicalAddGroup.toContinuousAdd RingHomCompTriple.ids exists_out_continuousLinearMap
mk_comp_outCLM 📖	mathematical	—	SeparationQuotient DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSeparationQuotient instAddCommMonoid AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instModule ContinuousLinearMap.funLike outCLM	—	IsTopologicalAddGroup.toContinuousAdd mk_outCLM
mk_outCLM 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring SeparationQuotient instTopologicalSpaceSeparationQuotient instAddCommMonoid AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instModule ContinuousLinearMap.funLike outCLM	—	DFunLike.congr_fun IsTopologicalAddGroup.toContinuousAdd RingHomCompTriple.ids mkCLM_comp_outCLM
outCLM_injective 📖	mathematical	—	SeparationQuotient DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSeparationQuotient instAddCommMonoid AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instModule ContinuousLinearMap.funLike outCLM	—	Topology.IsEmbedding.injective IsTopologicalAddGroup.toContinuousAdd isEmbedding_outCLM
outCLM_isUniformEmbedding 📖	mathematical	—	IsUniformEmbedding SeparationQuotient UniformSpace.toTopologicalSpace instUniformSpace DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSeparationQuotient instAddCommMonoid AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup IsUniformAddGroup.to_topologicalAddGroup instModule ContinuousLinearMap.funLike outCLM	—	IsTopologicalAddGroup.toContinuousAdd IsUniformAddGroup.to_topologicalAddGroup outCLM_isUniformInducing outCLM_injective
outCLM_isUniformInducing 📖	mathematical	—	IsUniformInducing SeparationQuotient UniformSpace.toTopologicalSpace instUniformSpace DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSeparationQuotient instAddCommMonoid AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup IsUniformAddGroup.to_topologicalAddGroup instModule ContinuousLinearMap.funLike outCLM	—	IsTopologicalAddGroup.toContinuousAdd IsUniformAddGroup.to_topologicalAddGroup IsUniformInducing.isUniformInducing_comp_iff mk_comp_outCLM IsUniformInducing.id
outCLM_uniformContinuous 📖	mathematical	—	UniformContinuous SeparationQuotient UniformSpace.toTopologicalSpace instUniformSpace DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSeparationQuotient instAddCommMonoid AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup IsUniformAddGroup.to_topologicalAddGroup instModule ContinuousLinearMap.funLike outCLM	—	IsUniformInducing.uniformContinuous IsTopologicalAddGroup.toContinuousAdd IsUniformAddGroup.to_topologicalAddGroup outCLM_isUniformInducing
postcomp_mkCLM_surjective 📖	mathematical	—	ContinuousLinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid SeparationQuotient instTopologicalSpaceSeparationQuotient instAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instModule ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.right_ids mkCLM	—	IsTopologicalAddGroup.toContinuousAdd RingHomCompTriple.right_ids RingHomCompTriple.ids ContinuousLinearMap.comp_assoc mkCLM_comp_outCLM ContinuousLinearMap.id_comp

---

← Back to Index