isOpen_iff_generate_intervals — Mathlib

English

For an OrderTopology α, a set s ⊆ α is open iff it belongs to the topology generated from the family of sets { Ioi(a), Iio(a) }.

Русский

Для OrderTopology α множество s ⊆ α открыто тогда и только тогда, когда оно относится к топологии, порождаемой семейством Ioi(a), Iio(a).

LaTeX

$$$\\text{IsOpen}(s) \\iff \\text{GenerateOpen}\\{ s \\mid \\exists a, s = Ioi(a) \\lor s = Iio(a) \\} s$$$

Lean4

theorem isOpen_iff_generate_intervals [t : OrderTopology α] {s : Set α} :
    IsOpen s ↔ GenerateOpen {s | ∃ a, s = Ioi a ∨ s = Iio a} s := by rw [t.topology_eq_generate_intervals]; rfl

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