isClosed_ball — Mathlib

English

In an ultrametric space, open balls are closed; equivalently, balls are clopen.

Русский

В ультраметрическом пространстве открытые шары являются закрытыми; шарa, следовательно, открыты и замкнуты.

LaTeX

$$\overline{\mathrm{ball}}(x,r) = \mathrm{ball}(x,r) \\ or \\ \overline{\mathrm{ball}}(x,r) = \mathrm{ball}(x,r)$$

Lean4

theorem isClosed_ball (x : X) (r : ℝ) : IsClosed (ball x r) := by
  cases le_or_gt r 0 with
  | inl hr => simp [ball_eq_empty.mpr hr]
  | inr h =>
    rw [← isOpen_compl_iff, isOpen_iff]
    simp only [Set.mem_compl_iff, gt_iff_lt]
    intro y hy
    cases ball_eq_or_disjoint x y r with
    | inl hd =>
      rw [hd] at hy
      simp [h.not_ge] at hy
    | inr hd =>
      use r
      simp [h, ← Set.le_iff_subset, le_compl_iff_disjoint_left, hd]

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