Baire theorem

In a complete metric space, a countable intersection of dense open subsets is dense.

The good concept underlying the theorem 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 prove Baire theorem, giving several different formulations that can be handy. 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.

class BaireSpace (X : Type u_4) [TopologicalSpace X] : Prop

The property BaireSpace α means that the topological space α has the Baire property: any countable intersection of open dense subsets is dense. Formulated here when the source space is ℕ (and subsumed below by dense_iInter_of_isOpen working with any encodable source space).

• baire_property : ∀ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ (n : ℕ), f n)

instance BaireSpace.of_pseudoEMetricSpace_completeSpace {X : Type u_1} [PseudoEMetricSpace X] [CompleteSpace X] : BaireSpace X

Baire theorems asserts that various topological spaces have the Baire property. Two versions of these theorems are given. The first states that complete PseudoEMetricSpaces are Baire.

Equations

• (_ : BaireSpace X) = (_ : BaireSpace X)

instance BaireSpace.of_t2Space_locallyCompactSpace {X : Type u_1} [TopologicalSpace X] [R1Space X] [LocallyCompactSpace X] : BaireSpace X

The second theorem states that locally compact R₁ spaces are Baire.

Equations

• (_ : BaireSpace X) = (_ : BaireSpace X)

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 : Set.Countable S) (hd : ∀ s ∈ S, Dense s) : Dense (⋂₀ S)

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 : Set.Countable S) (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 : Set.Countable S) (hd : ∀ s ∈ S, Dense s) : Dense (⋂₀ S)

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 : Set.Countable S) (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 : Set.Countable t) {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 : Set.Countable T) (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 ⋃₀.

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 : Set.Countable S) (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 : Set.Countable S) (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 ⋃₀.

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 : ι), Set.Nonempty (interior (f i))

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.