# mathlibdocumentation

topology.metric_space.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.

The names of the theorems do not contain the string "Baire", but are instead built from the form of the statement. "Baire" is however in the docstring of all the theorems, to facilitate grep searches.

We also define the filter residual α generated by dense Gδ sets and prove that this filter has the countable intersection property.

theorem dense_Inter_of_open_nat {α : Type u_1} {f : set α} (ho : ∀ (n : ), is_open (f n)) (hd : ∀ (n : ), dense (f n)) :
dense (⋂ (n : ), f n)

Baire theorem: a countable intersection of dense open sets is dense. Formulated here when the source space is ℕ (and subsumed below by dense_Inter_of_open working with any encodable source space).

theorem dense_sInter_of_open {α : Type u_1} {S : set (set α)} (ho : ∀ (s : set α), s S) (hS : S.countable) (hd : ∀ (s : set α), s S) :

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

theorem dense_bInter_of_open {α : Type u_1} {β : Type u_2} {S : set β} {f : β → set α} (ho : ∀ (s : β), s Sis_open (f s)) (hS : S.countable) (hd : ∀ (s : β), s Sdense (f s)) :
dense (⋂ (s : β) (H : 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_Inter_of_open {α : Type u_1} {β : Type u_2} [encodable β] {f : β → set α} (ho : ∀ (s : β), is_open (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 dense_sInter_of_Gδ {α : Type u_1} {S : set (set α)} (ho : ∀ (s : set α), s S) (hS : S.countable) (hd : ∀ (s : set α), s S) :

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

theorem dense_Inter_of_Gδ {α : Type u_1} {β : Type u_2} [encodable β] {f : β → set α} (ho : ∀ (s : β), is_Gδ (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_bInter_of_Gδ {α : Type u_1} {β : Type u_2} {S : set β} {f : Π (x : β), x Sset α} (ho : ∀ (s : β) (H : s S), is_Gδ (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δ {α : Type u_1} {s t : set α} (hs : is_Gδ s) (ht : is_Gδ t) (hsc : dense s) (htc : dense t) :
dense (s t)

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

theorem eventually_residual {α : Type u_1} {p : α → Prop} :
(∀ᶠ (x : α) in , p x) ∃ (t : set α), ∀ (x : α), x tp x

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

theorem mem_residual {α : Type u_1} {s : set α} :
s ∃ (t : set α) (H : t s),

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

theorem dense_of_mem_residual {α : Type u_1} {s : set α} (hs : s ) :
@[protected, instance]
def residual.countable_Inter_filter {α : Type u_1}  :
theorem dense_bUnion_interior_of_closed {α : Type u_1} {β : Type u_2} {S : set β} {f : β → set α} (hc : ∀ (s : β), s Sis_closed (f s)) (hS : S.countable) (hU : (⋃ (s : β) (H : s S), f s) = set.univ) :
dense (⋃ (s : β) (H : 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 : S.countable) (hU : ⋃₀S = set.univ) :
dense (⋃ (s : set α) (H : 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_Union_interior_of_closed {α : Type u_1} {β : Type u_2} [encodable β] {f : β → set α} (hc : ∀ (s : β), is_closed (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_Union_of_closed {α : Type u_1} {β : Type u_2} [nonempty α] [encodable β] {f : β → set α} (hc : ∀ (s : β), is_closed (f s)) (hU : (⋃ (s : β), f s) = set.univ) :
∃ (s : β), (interior (f s)).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.