isOpen_iff_generate_Iic_compl — Mathlib

English

A set is open in the upper topology iff it is generated by the complements of Iic a intervals.

Русский

Множество открыто в верхней топологии тогда и только тогда, когда оно порождается дополнениями интервалов Iic a.

LaTeX

$$$\\text{IsOpen}(s) \\iff \\mathrm{GenerateOpen}\\{t \\mid \\exists a, (\\Iic(a))^{c} = t\\} (s)$$$

Lean4

theorem isOpen_iff_generate_Iic_compl : IsOpen s ↔ GenerateOpen {t | ∃ a, (Iic a)ᶜ = t} s := by rw [topology_eq α]; rfl

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