mem_ball_iff — Mathlib

English

Membership of a in the ArchimedeanClass ball is equivalent to a strict inequality of mk a against the top.

Русский

Членство элемента a в шаре ArchimedeanClass эквивалентно строгому неравенству mk a против верхнего класса.

LaTeX

$$$a \in \text{ball } K c \iff c < \mathrm{mk}(a)$$$

Lean4

@[simp]
theorem mem_ball_iff {a : M} {c : ArchimedeanClass M} (hc : c ≠ ⊤) : a ∈ ball K c ↔ c < mk a :=
  mem_ballAddSubgroup_iff hc

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