not_isMeagre_of_isGδ_of_dense — Mathlib

English

In a nonempty Baire space, every dense Gδ set is not meagre.

Русский

В не пустом Бэре-пространстве любой плотный множество типа Gδ не является слабой (meagre).

LaTeX

$$not_isMeagre_of_isGδ_of_dense {s : Set X} (hs : IsGδ s) (hd : Dense s) : ¬IsMeagre s$$

Lean4

/-- In a nonempty Baire space, any dense `Gδ` set is not meagre. -/
theorem not_isMeagre_of_isGδ_of_dense {s : Set X} (hs : IsGδ s) (hd : Dense s) : ¬IsMeagre s :=
  by
  intro h
  rcases (mem_residual).1 h with ⟨t, hts, htG, hd'⟩
  rcases (hd.inter_of_Gδ hs htG hd').nonempty with ⟨x, hx₁, hx₂⟩
  exact hts hx₂ hx₁

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