mathlib documentation

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 sets and prove that this filter has the countable intersection property.

def is_Gδ {α : Type u_1} [topological_space α] :
set α → Prop

A Gδ set is a countable intersection of open sets.

Equations
theorem is_open.is_Gδ {α : Type u_1} [topological_space α] {s : set α} :
is_open sis_Gδ s

An open set is a Gδ set.

theorem is_Gδ_univ {α : Type u_1} [topological_space α] :

theorem is_Gδ_bInter_of_open {α : Type u_1} {ι : Type u_4} [topological_space α] {I : set ι} (hI : I.countable) {f : ι → set α} :
(∀ (i : ι), i Iis_open (f i))is_Gδ (⋂ (i : ι) (H : i I), f i)

theorem is_Gδ_Inter_of_open {α : Type u_1} {ι : Type u_4} [topological_space α] [encodable ι] {f : ι → set α} :
(∀ (i : ι), is_open (f i))is_Gδ (⋂ (i : ι), f i)

theorem is_Gδ_sInter {α : Type u_1} [topological_space α] {S : set (set α)} :
(∀ (s : set α), s Sis_Gδ s)S.countableis_Gδ (⋂₀S)

A countable intersection of Gδ sets is a Gδ set.

theorem is_Gδ_Inter {α : Type u_1} {ι : Type u_4} [topological_space α] [encodable ι] {s : ι → set α} :
(∀ (i : ι), is_Gδ (s i))is_Gδ (⋂ (i : ι), s i)

theorem is_Gδ_bInter {α : Type u_1} {ι : Type u_4} [topological_space α] {s : set ι} (hs : s.countable) {t : Π (i : ι), i sset α} :
(∀ (i : ι) (H : i s), is_Gδ (t i H))is_Gδ (⋂ (i : ι) (H : i s), t i H)

theorem is_Gδ.inter {α : Type u_1} [topological_space α] {s t : set α} :
is_Gδ sis_Gδ tis_Gδ (s t)

theorem is_Gδ.union {α : Type u_1} [topological_space α] {s t : set α} :
is_Gδ sis_Gδ tis_Gδ (s t)

The union of two Gδ sets is a Gδ set.

def residual (α : Type u_1) [topological_space α] :

A set s is called residual if it includes a dense set. If α is a Baire space (e.g., a complete metric space), then residual sets form a filter, see mem_residual.

For technical reasons we define the filter residual in any topological space but in a non-Baire space it is not useful because it may contain some non-residual sets.

Equations
theorem dense_Inter_of_open_nat {α : Type u_1} [emetric_space α] [complete_space α] {f : set α} :
(∀ (n : ), is_open (f n))(∀ (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} [emetric_space α] [complete_space α] {S : set (set α)} :
(∀ (s : set α), s Sis_open s)S.countable(∀ (s : set α), s Sdense s)dense (⋂₀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} [emetric_space α] [complete_space α] {S : set β} {f : β → set α} :
(∀ (s : β), s Sis_open (f s))S.countable(∀ (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} [emetric_space α] [complete_space α] [encodable β] {f : β → set α} :
(∀ (s : β), is_open (f s))(∀ (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} [emetric_space α] [complete_space α] {S : set (set α)} :
(∀ (s : set α), s Sis_Gδ s)S.countable(∀ (s : set α), s Sdense s)dense (⋂₀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} [emetric_space α] [complete_space α] [encodable β] {f : β → set α} :
(∀ (s : β), is_Gδ (f s))(∀ (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} [emetric_space α] [complete_space α] {S : set β} {f : Π (x : β), x Sset α} :
(∀ (s : β) (H : s S), is_Gδ (f s H))S.countable(∀ (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} [emetric_space α] [complete_space α] {s t : set α} :
is_Gδ sis_Gδ tdense sdense tdense (s t)

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

theorem eventually_residual {α : Type u_1} [emetric_space α] [complete_space α] {p : α → Prop} :
(∀ᶠ (x : α) in residual α, p x) ∃ (t : set α), is_Gδ t dense t ∀ (x : α), x tp x

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

theorem mem_residual {α : Type u_1} [emetric_space α] [complete_space α] {s : set α} :
s residual α ∃ (t : set α) (H : t s), is_Gδ t dense t

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

theorem dense_bUnion_interior_of_closed {α : Type u_1} {β : Type u_2} [emetric_space α] [complete_space α] {S : set β} {f : β → set α} :
(∀ (s : β), s Sis_closed (f s))S.countable(⋃ (s : β) (H : s S), f s) = set.univdense (⋃ (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} [emetric_space α] [complete_space α] {S : set (set α)} :
(∀ (s : set α), s Sis_closed s)S.countable⋃₀S = set.univdense (⋃ (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} [emetric_space α] [complete_space α] [encodable β] {f : β → set α} :
(∀ (s : β), is_closed (f s))(⋃ (s : β), f s) = set.univdense (⋃ (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} [emetric_space α] [complete_space α] [nonempty α] [encodable β] {f : β → set α} :
(∀ (s : β), is_closed (f s))(⋃ (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.