norm_lt_iff

Mathlib.Analysis.Normed.Group.Quotient

URI: https://scilib.ai/kg/mathlib#QuotientGroup.norm_lt_iff

English

For any quotient x, ∥x∥ < r if and only if there exists m with mk m = x and ∥m∥ < r.

Русский

Для любого x существует m с mk m = x и ∥m∥ < r тогда, когда ∥x∥ < r.

LaTeX

$$$\|x\| < r \;\Leftrightarrow\; \exists m, \; \text{mk } m = x \land \|m\| < r$$$

Lean4

@[to_additive]
theorem norm_lt_iff : ‖x‖ < r ↔ ∃ m : M, ↑m = x ∧ ‖m‖ < r := by simp [norm_eq_infDist, infDist_lt_iff (norm_aux _)]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru