mem_emetric_ball_one_iff — Mathlib

English

In a seminormed group with EN-norm, the open ball of radius r around the identity element 1 for the EMetric coincides with the set of all a in E whose EN-norm is less than r; that is, a ∈ EMetric.ball 1 r if and only if ‖a‖ₑ < r.

Русский

В полугруппе с EN-нормой открытый шар радиуса r вокруг единицы по EMetric совпадает с множеством элементов a ∈ E such that ‖a‖ₑ < r; то есть a ∈ EMetric.ball 1 r тогда и только тогда, когда ‖a‖ₑ < r.

LaTeX

$$$a \\in \\mathrm{EMetric.ball}(1,r) \\iff \\|a\\|_{\\varepsilon} < r$$$

Lean4

@[to_additive]
theorem mem_emetric_ball_one_iff {r : ℝ≥0∞} : a ∈ EMetric.ball 1 r ↔ ‖a‖ₑ < r := by
  rw [EMetric.mem_ball, edist_one_eq_enorm]

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