# Documentation

Mathlib.Topology.MetricSpace.Baire

# 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) [] :

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

Instances

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.

The second theorem states that locally compact spaces are Baire.

theorem dense_iInter_of_open_nat {α : Type u_1} [] [] {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} [] [] {S : Set (Set α)} (ho : ∀ (s : Set α), s S) (hS : ) (hd : ∀ (s : Set α), s 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} [] [] {S : Set β} {f : βSet α} (ho : ∀ (s : β), s SIsOpen (f s)) (hS : ) (hd : ∀ (s : β), s SDense (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} [] [] [] {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} [] [] {s : Set α} :
s t x, IsGδ t

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

theorem eventually_residual {α : Type u_1} [] [] {p : αProp} :
(∀ᶠ (x : α) in , p x) t, IsGδ t ((x : α) → x tp 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} [] [] {s : Set α} (hs : s ) :
theorem dense_sInter_of_Gδ {α : Type u_1} [] [] {S : Set (Set α)} (ho : ∀ (s : Set α), s SIsGδ s) (hS : ) (hd : ∀ (s : Set α), s 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} [] [] [] {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} [] [] {S : Set β} {f : (x : β) → x SSet α} (ho : ∀ (s : β) (H : s S), IsGδ (f s H)) (hS : ) (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} [] [] {s : Set α} {t : Set α} (hs : IsGδ s) (ht : IsGδ t) (hsc : ) (htc : ) :
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} [] [] [] {s : Set α} (hs : IsGδ s) (hd : ) {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} [] [] {t : Set ι} {s : Set α} (hs : IsGδ s) (hd : ) (ht : ) {f : ιSet α} (hc : ∀ (i : ι), i tIsClosed (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} [] [] {T : Set (Set α)} {s : Set α} (hs : IsGδ s) (hd : ) (hc : ) (hc' : ∀ (t : Set α), t T) (hU : s ⋃₀ T) :
Dense (⋃ (t : Set α) (_ : t 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} [] [] {S : Set β} {f : βSet α} (hc : ∀ (s : β), s SIsClosed (f s)) (hS : ) (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} [] [] {S : Set (Set α)} (hc : ∀ (s : Set α), s S) (hS : ) (hU : ⋃₀ S = Set.univ) :
Dense (⋃ (s : Set α) (_ : s 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} [] [] [] {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} [] [] [] [] {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.