norm_le — Mathlib

English

For a quotient map f, and any m ∈ M, we have ‖f(m)‖ ≤ ‖m‖.

Русский

Для отображения-фактора f выполняется неравенство ‖f(m)‖ ≤ ‖m‖ для каждого m∈M.

LaTeX

$$$\\|f m\\| \\le \\|m\\| \\quad\\text{for all } m\\in M$$$

Lean4

theorem norm_le {f : NormedAddGroupHom M N} (hquot : IsQuotient f) (m : M) : ‖f m‖ ≤ ‖m‖ :=
  by
  rw [hquot.norm]
  apply csInf_le
  · use 0
    rintro _ ⟨m', -, rfl⟩
    apply norm_nonneg
  · exact ⟨0, f.ker.zero_mem, by simp⟩

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