exists_norm_mk_lt — Mathlib

English

For any x in the quotient and any 0 < ε, there exists m in M with mk' S m = x and ∥m∥ < ∥x∥ + ε.

Русский

Для любого x в фактор-группе и любого ε > 0 существует m в M с mk' S m = x и ∥m∥ < ∥x∥ + ε.

LaTeX

$$$\exists m : M, m = x ∧ \|m\| < \|x\| + ε$$$

Lean4

/-- For any `x : M ⧸ S` and any `0 < ε`, there is `m : M` such that `mk' S m = x`
and `‖m‖ < ‖x‖ + ε`. -/
@[to_additive /-- For any `x : M ⧸ S` and any `0 < ε`, there is `m : M` such that `mk' S m = x`
    and `‖m‖ < ‖x‖ + ε`. -/
    ]
theorem exists_norm_mk_lt (x : M ⧸ S) (hε : 0 < ε) : ∃ m : M, m = x ∧ ‖m‖ < ‖x‖ + ε :=
  norm_lt_iff.1 <| lt_add_of_pos_right _ hε

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