isClosed_ball_top — Mathlib

English

The ball with radius top (∞) around x is the whole space, hence closed.

Русский

Шар с радиусом топ (∞) вокруг x есть вся пространства, значит замкнут.

LaTeX

$$$\\mathrm{IsClosed}(\\mathrm{ball}(x,\\top))$$$

Lean4

theorem isClosed_ball_top : IsClosed (ball x ⊤) :=
  isOpen_compl_iff.1 <|
    isOpen_iff.2 fun _y hy =>
      ⟨⊤, ENNReal.coe_lt_top, fun _z hzy hzx => hy (edistLtTopSetoid.trans (edistLtTopSetoid.symm hzy) hzx)⟩

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