iInter_of_isOpen — Mathlib

English

A set is Gδ if and only if it is a countable intersection of a sequence of open sets.

Русский

Множество есть Gδ тогда и только тогда, когда оно есть счетное пересечение последовательности открытых множеств.

LaTeX

$$$IsGδ(s)\\iff \\exists f: \\mathbb{N}\\to Set(X), (\\forall n, IsOpen(f(n))) \\land s=\\bigcap_{n\\in\\mathbb{N}} f(n)$$$

Lean4

theorem iInter_of_isOpen [Countable ι'] {f : ι' → Set X} (hf : ∀ i, IsOpen (f i)) : IsGδ (⋂ i, f i) :=
  ⟨range f, by rwa [forall_mem_range], countable_range _, by rw [sInter_range]⟩

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