norm_mk_lt — Mathlib

English

For any x in M/S and ε>0, there exists m in M with mk m = x and ‖m‖ < ‖x‖ + ε.

Русский

Для любого x ∈ M/S и ε>0 существует m ∈ M с mk m = x и ‖m‖ < ‖x‖ + ε.

LaTeX

$$$\\exists m : M, Submodule.Quotient.mk m = x \\land \\|m\\| < \\|x\\| + \\varepsilon$$$

Lean4

/-- For any `x : M ⧸ S` and any `0 < ε`, there is `m : M` such that `Submodule.Quotient.mk m = x`
and `‖m‖ < ‖x‖ + ε`. -/
nonrec theorem norm_mk_lt {S : Submodule R M} (x : M ⧸ S) {ε : ℝ} (hε : 0 < ε) :
    ∃ m : M, Submodule.Quotient.mk m = x ∧ ‖m‖ < ‖x‖ + ε :=
  exists_norm_mk_lt x hε

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