isOpen_def — Mathlib

English

In OnePoint X, a set s is open if and only if either a certain compactness condition holds when ∞ ∈ s, or the preimage is open in X; precisely: IsOpen s ↔ (∞ ∈ s → IsCompact i^{-1}(s)^c) ∧ IsOpen i^{-1}(s).

Русский

Во множестве OnePoint X множество s открыто тогда и только тогда, когда выполняется условие компактности при ∞ ∈ s или обратное изображение открыто в X; точно: IsOpen s ↔ (∞ ∈ s → IsCompact i^{-1}(s)^c) ∧ IsOpen i^{-1}(s).

LaTeX

$$$\\mathrm{IsOpen}(s) \\iff (\\infty \\in s \\to \\operatorname{IsCompact}(i^{-1}(s))^{c}) \\land \\mathrm{IsOpen}(i^{-1}(s)).$$$

Lean4

theorem isOpen_def : IsOpen s ↔ (∞ ∈ s → IsCompact ((↑) ⁻¹' s : Set X)ᶜ) ∧ IsOpen ((↑) ⁻¹' s : Set X) :=
  Iff.rfl

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