isOpen_ne_top — Mathlib

English

In the extended nonnegative real line, the subset of finite elements {a ∈ ℝ≥0∞ : a ≠ ∞} is open.

Русский

В расширенной полугиперреальной прямой множество конечных элементов {a ∈ ℝ≥0∞ : a ≠ ∞} открыто.

LaTeX

$$$\\operatorname{IsOpen}\\{a \\in \\mathbb{R}_{\\ge 0}^{\\infty} \\mid a \\neq \\infty\\}$$$

Lean4

theorem isOpen_ne_top : IsOpen {a : ℝ≥0∞ | a ≠ ∞} :=
  isOpen_ne

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