le_norm_iff — Mathlib

English

For any quotient x and real r, r ≤ ∥x∥ if and only if for all representatives m with mk m = x, r ≤ ∥m∥.

Русский

Для любой величины r ≤ ∥x∥ равно тому, что для всех представителей m с mk m = x, выполняется r ≤ ∥m∥.

LaTeX

$$$r \le \|x\| \;\Longleftrightarrow\; \forall m, \; \big(\text{mk } m = x \big) \rightarrow r \le \|m\|$$$

Lean4

@[to_additive]
theorem le_norm_iff : r ≤ ‖x‖ ↔ ∀ m : M, ↑m = x → r ≤ ‖m‖ := by simp [norm_eq_infDist, le_infDist (norm_aux _)]

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