Theorems · Theorem · general topology

not_isMeagre_of_isOpen

∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] {s : Set X}, IsOpen s → s.Nonempty → ¬IsMeagre s

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.

Defined in

Mathlib.Topology.Baire.Lemmas

Cited by

0 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceBaireSpace