norm_mk_lt — Mathlib

English

For any x ∈ R/ I and ε>0, there exists r ∈ R with mk I r = x and ∥r∥ < ∥x∥ + ε.

Русский

Для любого x ∈ R/I и ε>0 существует r ∈ R с mk I r = x и ∥r∥ < ∥x∥ + ε.

LaTeX

$$$\\exists r : R, Ideal.Quotient.mk I r = x \\land \\|r\\| < \\|x\\| + ε$$$

Lean4

nonrec theorem norm_mk_lt {I : Ideal R} (x : R ⧸ I) {ε : ℝ} (hε : 0 < ε) :
    ∃ r : R, Ideal.Quotient.mk I r = x ∧ ‖r‖ < ‖x‖ + ε :=
  exists_norm_mk_lt x hε

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