ball_le_closedBall — Mathlib

English

For every ArchimedeanClass c in M, the open ball is contained in the corresponding closed ball: Ball_K(c) ⊆ ClosedBall_K(c).

Русский

Для каждой ArchimedeanClass c в M выполняется включение открытого шара в соответствующий закрытый шар: Ball_K(c) ⊆ ClosedBall_K(c).

LaTeX

$$$\\forall c\\, \\mathrm{ball}_{K}(c) \\subseteq \\mathrm{closedBall}_{K}(c).$$$

Lean4

theorem ball_le_closedBall {c : ArchimedeanClass M} : ball K c ≤ closedBall K c :=
  by
  obtain rfl | hc := eq_or_ne c ⊤
  · simp
  intro a ha
  simpa using ((mem_ball_iff K hc).mp ha).le

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