not_isMeagre_of_mem_residual — Mathlib

English

In a nonempty Baire space, a residual set is not meagre.

Русский

В не пустом пространстве Бэра множество, содержащееся в резидуа́льной (r esidual) части, не является слабым (meagre).

LaTeX

$$not_isMeagre_of_mem_residual {s : Set X} (hs : s ∈ residual X) : ¬IsMeagre s$$

Lean4

/-- In a nonempty Baire space, a residual set is not meagre. -/
theorem not_isMeagre_of_mem_residual {s : Set X} (hs : s ∈ residual X) : ¬IsMeagre s :=
  by
  rcases (mem_residual (X := X)).1 hs with ⟨t, ht_sub, htGδ, ht_dense⟩
  intro hs_meagre
  exact not_isMeagre_of_isGδ_of_dense (X := X) htGδ ht_dense (hs_meagre.mono ht_sub)

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