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 (α : Type u_5) [TopologicalSpace α] : Prop

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

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_open working with any encodable source space).

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

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.of_pseudoEMetricSpace_completeSpace = @BaireSpace.of_pseudoEMetricSpace_completeSpace.proof_1

instance BaireSpace.of_t2Space_locallyCompactSpace {α : Type u_1} [TopologicalSpace α] [T2Space α] [LocallyCompactSpace α] : BaireSpace α

The second theorem states that locally compact spaces are Baire.

Equations

• @BaireSpace.of_t2Space_locallyCompactSpace = @BaireSpace.of_t2Space_locallyCompactSpace.proof_1

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

Definition of a Baire space.

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

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

theorem dense_biInter_of_open {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [BaireSpace α] {S : Set β} {f : β → Set α} (ho : ∀ (s : β), s ∈ S → IsOpen (f s)) (hS : Set.Countable S) (hd : ∀ (s : β), s ∈ S → Dense (f s)) : Dense (⋂ (s : β) (_ : 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_open {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [BaireSpace α] [Encodable β] {f : β → Set α} (ho : ∀ (s : β), IsOpen (f s)) (hd : ∀ (s : β), Dense (f s)) : Dense (⋂ (s : β), f s)

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

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

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

theorem eventually_residual {α : Type u_1} [TopologicalSpace α] [BaireSpace α] {p : α → Prop} : (∀ᶠ (x : α) in residual α, p x) ↔ ∃ t, IsGδ t ∧ Dense t ∧ ((x : α) → 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 {α : Type u_1} [TopologicalSpace α] [BaireSpace α] {s : Set α} (hs : s ∈ residual α) : Dense s

theorem dense_sInter_of_Gδ {α : Type u_1} [TopologicalSpace α] [BaireSpace α] {S : Set (Set α)} (ho : ∀ (s : Set α), s ∈ S → IsGδ s) (hS : Set.Countable S) (hd : ∀ (s : Set α), 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δ {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [BaireSpace α] [Encodable β] {f : β → Set α} (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 an encodable type.

theorem dense_biInter_of_Gδ {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [BaireSpace α] {S : Set β} {f : (x : β) → x ∈ S → Set α} (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δ {α : Type u_1} [TopologicalSpace α] [BaireSpace α] {s : Set α} {t : Set α} (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 {α : Type u_1} {ι : Type u_4} [TopologicalSpace α] [BaireSpace α] [Encodable ι] {s : Set α} (hs : IsGδ s) (hd : Dense s) {f : ι → Set α} (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 {α : Type u_1} {ι : Type u_4} [TopologicalSpace α] [BaireSpace α] {t : Set ι} {s : Set α} (hs : IsGδ s) (hd : Dense s) (ht : Set.Countable t) {f : ι → Set α} (hc : ∀ (i : ι), i ∈ t → IsClosed (f i)) (hU : s ⊆ ⋃ (i : ι) (_ : i ∈ t), f i) : Dense (⋃ (i : ι) (_ : 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 {α : Type u_1} [TopologicalSpace α] [BaireSpace α] {T : Set (Set α)} {s : Set α} (hs : IsGδ s) (hd : Dense s) (hc : Set.Countable T) (hc' : ∀ (t : Set α), t ∈ T → IsClosed t) (hU : s ⊆ ⋃₀ T) : Dense (⋃ (t : Set α) (_ : 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 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [BaireSpace α] {S : Set β} {f : β → Set α} (hc : ∀ (s : β), s ∈ S → IsClosed (f s)) (hS : Set.Countable S) (hU : ⋃ (s : β) (_ : s ∈ S), f s = Set.univ) : Dense (⋃ (s : β) (_ : 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 {α : Type u_1} [TopologicalSpace α] [BaireSpace α] {S : Set (Set α)} (hc : ∀ (s : Set α), s ∈ S → IsClosed s) (hS : Set.Countable S) (hU : ⋃₀ S = Set.univ) : Dense (⋃ (s : Set α) (_ : 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 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [BaireSpace α] [Encodable β] {f : β → Set α} (hc : ∀ (s : β), IsClosed (f s)) (hU : ⋃ (s : β), f s = Set.univ) : Dense (⋃ (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 an encodable type.

theorem nonempty_interior_of_iUnion_of_closed {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [BaireSpace α] [Nonempty α] [Encodable β] {f : β → Set α} (hc : ∀ (s : β), IsClosed (f s)) (hU : ⋃ (s : β), f s = Set.univ) : ∃ s, Set.Nonempty (interior (f s))

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.