surjective_normedMk — Mathlib

English

For any AddSubgroup S of a seminormed additive group M, the normedMk map is surjective onto the quotient space M/S.

Русский

Для любого подгруппового дополнения S в семинометрированной абелевой группе M, отображение normedMk сюръективно на частный пространство M/S.

LaTeX

$$$\text{normedMk}_S: M \to M/S \text{ is surjective.}$$$

Lean4

/-- `S.normedMk` is surjective. -/
theorem surjective_normedMk (S : AddSubgroup M) : Function.Surjective (normedMk S) :=
  Quot.mk_surjective

Похожие утверждения