IsGδ — Mathlib

English

A Gδ set is a countable intersection of open sets.

Русский

Gδ-множество — это счетное пересечение открытых множеств.

LaTeX

$$$IsGδ(s)\\iff\\exists T\\subseteq Set(X), (\\forall t\\in T, IsOpen(t)) \\land Countable(T) \\land s=\\bigcap_{t\\in T} t$$$

Lean4

/-- A Gδ set is a countable intersection of open sets. -/
def IsGδ (s : Set X) : Prop :=
  ∃ T : Set (Set X), (∀ t ∈ T, IsOpen t) ∧ T.Countable ∧ s = ⋂₀ T

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