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.

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.

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.sInter

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

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.

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.

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.

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.

theorem dense_of_mem_residual {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {s : Set X} (hs : s ∈ residual X) : Dense s

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.sInter

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

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.

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.

theorem Dense.inter_of_Gδ {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {s : Set X} {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.

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 ⋃.

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.

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.sUnion) : 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 ⋃₀.

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.

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.sUnion = 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 ⋃₀.

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.

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.