English
In a Baire space, every nonempty open set is non-meagre (cannot be a countable union of nowhere-dense sets).
Русский
В пространстве Баире любое непустое открытое множество не является мелким (не может быть выражено как счетное объединение нигде плотных множеств).
LaTeX
$$$\\neg\\big( \\text{IsMeagre}(s) \\big)$, если $s$ открыто и непусто.$$
Lean4
/-- In a Baire space, every nonempty open set is non‐meagre,
that is, it cannot be written as a countable union of nowhere‐dense sets.
-/
theorem not_isMeagre_of_isOpen {s : Set X} (hs : IsOpen s) (hne : s.Nonempty) : ¬IsMeagre s :=
by
intro h
obtain ⟨x, hx, hxc⟩ := (dense_of_mem_residual (by rwa [IsMeagre] at h)).inter_open_nonempty s hs hne
exact hxc hx
