inter_of_Gδ — Mathlib

English

The intersection of two dense Gδ sets is dense.

Русский

Пересечение плотных Gδ-множеств остаётся плотным.

LaTeX

$$$\\\\forall s,t \\\\ IsGδ(s) \\\\land IsGδ(t) \\\\land Dense(s) \\\\land Dense(t) \\\\Rightarrow Dense(s \\cap t)$$$

Lean4

/-- Baire theorem: the intersection of two dense Gδ sets is dense. -/
theorem inter_of_Gδ {s t : Set X} (hs : IsGδ s) (ht : IsGδ t) (hsc : Dense s) (htc : Dense t) : Dense (s ∩ t) :=
  by
  rw [inter_eq_iInter]
  apply dense_iInter_of_Gδ <;> simp [Bool.forall_bool, *]

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