# Baire spaces #

A topological space is called a Baire space if a countable intersection of dense open subsets is dense. Baire theorems say that all completely metrizable spaces and all locally compact regular spaces are Baire spaces. We prove the theorems in `Mathlib/Topology/Baire/CompleteMetrizable` and `Mathlib/Topology/Baire/LocallyCompactRegular`.

In this file we prove various corollaries of Baire theorems.

The good concept underlying the theorems is that of a Gδ set, i.e., a countable intersection of open sets. Then Baire theorem can also be formulated as the fact that a countable intersection of dense Gδ sets is a dense Gδ set. We deduce this version from Baire property. We also prove the important consequence that, if the space is covered by a countable union of closed sets, then the union of their interiors is dense.

We also prove that in Baire spaces, the `residual` sets are exactly those containing a dense Gδ set.

source
theorem dense_iInter_of_isOpen_nat {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {f : ℕ → Set X} (ho : ∀ (n : ℕ), IsOpen (f n)) (hd : ∀ (n : ℕ), Dense (f n)) :
Dense (⋂ (n : ℕ), f n)

Definition of a Baire space.

source
theorem dense_sInter_of_isOpen {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {S : Set (Set X)} (ho : ∀ s ∈ S, IsOpen s) (hS : S.Countable) (hd : ∀ s ∈ S, Dense s) :
Dense (⋂₀ S)

Baire theorem: a countable intersection of dense open sets is dense. Formulated here with ⋂₀.

source
theorem dense_biInter_of_isOpen {X : Type u_1} {α : Type u_2} [TopologicalSpace X] [BaireSpace X] {S : Set α} {f : α → Set X} (ho : ∀ s ∈ S, IsOpen (f s)) (hS : S.Countable) (hd : ∀ s ∈ S, Dense (f s)) :
Dense (⋂ s ∈ S, f s)

Baire theorem: a countable intersection of dense open sets is dense. Formulated here with an index set which is a countable set in any type.

source
theorem dense_iInter_of_isOpen {X : Type u_1} {ι : Sort u_3} [TopologicalSpace X] [BaireSpace X] [Countable ι] {f : ι → Set X} (ho : ∀ (i : ι), IsOpen (f i)) (hd : ∀ (i : ι), Dense (f i)) :
Dense (⋂ (s : ι), f s)

Baire theorem: a countable intersection of dense open sets is dense. Formulated here with an index set which is a countable type.

source
theorem mem_residual {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {s : Set X} :
s ∈ residual X ↔ ∃ t ⊆ s, IsGδ t ∧ Dense t

A set is residual (comeagre) if and only if it includes a dense `Gδ` set.

source
theorem eventually_residual {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {p : X → Prop} :
(∀ᶠ (x : X) in residual X, p x) ↔ ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x

A property holds on a residual (comeagre) set if and only if it holds on some dense `Gδ` set.

source
theorem dense_of_mem_residual {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {s : Set X} (hs : s ∈ residual X) :
Dense s
source
theorem not_isMeagre_of_isOpen {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {s : Set X} (hs : IsOpen s) (hne : 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.

source
theorem dense_sInter_of_Gδ {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {S : Set (Set X)} (ho : ∀ s ∈ S, IsGδ s) (hS : S.Countable) (hd : ∀ s ∈ S, Dense s) :
Dense (⋂₀ S)

Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with ⋂₀.

source
theorem dense_iInter_of_Gδ {X : Type u_1} {ι : Sort u_3} [TopologicalSpace X] [BaireSpace X] [Countable ι] {f : ι → Set X} (ho : ∀ (s : ι), IsGδ (f s)) (hd : ∀ (s : ι), Dense (f s)) :
Dense (⋂ (s : ι), f s)

Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with an index set which is a countable type.

source
theorem dense_biInter_of_Gδ {X : Type u_1} {α : Type u_2} [TopologicalSpace X] [BaireSpace X] {S : Set α} {f : (x : α) → x ∈ S → Set X} (ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)) (hS : S.Countable) (hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)) :
Dense (⋂ (s : α), ⋂ (h : s ∈ S), f s h)

Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with an index set which is a countable set in any type.

source
theorem Dense.inter_of_Gδ {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {s t : Set X} (hs : IsGδ s) (ht : IsGδ t) (hsc : Dense s) (htc : Dense t) :
Dense (s ∩ t)

Baire theorem: the intersection of two dense Gδ sets is dense.

source
theorem IsGδ.dense_iUnion_interior_of_closed {X : Type u_1} {ι : Sort u_3} [TopologicalSpace X] [BaireSpace X] [Countable ι] {s : Set X} (hs : IsGδ s) (hd : Dense s) {f : ι → Set X} (hc : ∀ (i : ι), IsClosed (f i)) (hU : s ⊆ ⋃ (i : ι), f i) :
Dense (⋃ (i : ι), interior (f i))

If a countable family of closed sets cover a dense `Gδ` set, then the union of their interiors is dense. Formulated here with `⋃`.

source
theorem IsGδ.dense_biUnion_interior_of_closed {X : Type u_1} {α : Type u_2} [TopologicalSpace X] [BaireSpace X] {t : Set α} {s : Set X} (hs : IsGδ s) (hd : Dense s) (ht : t.Countable) {f : α → Set X} (hc : ∀ i ∈ t, IsClosed (f i)) (hU : s ⊆ ⋃ i ∈ t, f i) :
Dense (⋃ i ∈ t, interior (f i))

If a countable family of closed sets cover a dense `Gδ` set, then the union of their interiors is dense. Formulated here with a union over a countable set in any type.

source
theorem IsGδ.dense_sUnion_interior_of_closed {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {T : Set (Set X)} {s : Set X} (hs : IsGδ s) (hd : Dense s) (hc : T.Countable) (hc' : ∀ t ∈ T, IsClosed t) (hU : s ⊆ ⋃₀ T) :
Dense (⋃ t ∈ T, interior t)

If a countable family of closed sets cover a dense `Gδ` set, then the union of their interiors is dense. Formulated here with `⋃₀`.

source
theorem dense_biUnion_interior_of_closed {X : Type u_1} {α : Type u_2} [TopologicalSpace X] [BaireSpace X] {S : Set α} {f : α → Set X} (hc : ∀ s ∈ S, IsClosed (f s)) (hS : S.Countable) (hU : ⋃ s ∈ S, f s = Set.univ) :
Dense (⋃ s ∈ S, interior (f s))

Baire theorem: if countably many closed sets cover the whole space, then their interiors are dense. Formulated here with an index set which is a countable set in any type.

source
theorem dense_sUnion_interior_of_closed {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {S : Set (Set X)} (hc : ∀ s ∈ S, IsClosed s) (hS : S.Countable) (hU : ⋃₀ S = Set.univ) :
Dense (⋃ s ∈ S, interior s)

Baire theorem: if countably many closed sets cover the whole space, then their interiors are dense. Formulated here with `⋃₀`.

source
theorem dense_iUnion_interior_of_closed {X : Type u_1} {ι : Sort u_3} [TopologicalSpace X] [BaireSpace X] [Countable ι] {f : ι → Set X} (hc : ∀ (i : ι), IsClosed (f i)) (hU : ⋃ (i : ι), f i = Set.univ) :
Dense (⋃ (i : ι), interior (f i))

Baire theorem: if countably many closed sets cover the whole space, then their interiors are dense. Formulated here with an index set which is a countable type.

source
theorem nonempty_interior_of_iUnion_of_closed {X : Type u_1} {ι : Sort u_3} [TopologicalSpace X] [BaireSpace X] [Nonempty X] [Countable ι] {f : ι → Set X} (hc : ∀ (i : ι), IsClosed (f i)) (hU : ⋃ (i : ι), f i = Set.univ) :
∃ (i : ι), (interior (f i)).Nonempty

One of the most useful consequences of Baire theorem: if a countable union of closed sets covers the space, then one of the sets has nonempty interior.

source
theorem not_isMeagre_of_isGδ_of_dense {X : Type u_1} [TopologicalSpace X] [BaireSpace X] [Nonempty X] {s : Set X} (hs : IsGδ s) (hd : Dense s) :
¬IsMeagre s

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

source
theorem not_isMeagre_of_mem_residual {X : Type u_1} [TopologicalSpace X] [BaireSpace X] [Nonempty X] {s : Set X} (hs : s ∈ residual X) :
¬IsMeagre s

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