isQuotientQuotient — Mathlib

English

The quotient map S.normedMk is an IsQuotient map (a genuine quotient map).

Русский

Координатное отображение $S.normedMk$ является факторной (квотируемой) отображением.

LaTeX

$$IsQuotient(S.normedMk)$$

Lean4

/-- `S.normedMk` satisfies `IsQuotient`. -/
theorem isQuotientQuotient (S : AddSubgroup M) : IsQuotient S.normedMk :=
  ⟨S.surjective_normedMk, fun m => by simpa [S.ker_normedMk] using quotient_norm_mk_eq _ m⟩

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