Theorems · Theorem · general topology

SeparationQuotient.mk_outCLM

∀ (K : Type u_1) {E : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup E] [inst_2 : Module K E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : ContinuousConstSMul K E]
  (x : SeparationQuotient E), SeparationQuotient.mk ((SeparationQuotient.outCLM K E) x) = x

Defined in

Mathlib.Topology.Algebra.SeparationQuotient.Section

Cited by

4 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousConstSMul