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.

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

@[class]
structure baire_space (α : Type u_5) [topological_space α] :
Prop

The property baire_space α 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_Inter_of_open working with any encodable source space).

Instances of this typeclass
@[protected, instance]

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

@[protected, instance]

The second theorem states that locally compact spaces are Baire.

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

Definition of a Baire space.

theorem dense_sInter_of_open {α : Type u_1} [topological_space α] [baire_space α] {S : set (set α)} (ho : ∀ (s : set α), s Sis_open s) (hS : S.countable) (hd : ∀ (s : set α), s Sdense 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} [topological_space α] [baire_space α] {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} [topological_space α] [baire_space α] [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} [topological_space α] [baire_space α] {S : set (set α)} (ho : ∀ (s : set α), s Sis_Gδ s) (hS : S.countable) (hd : ∀ (s : set α), s Sdense 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} [topological_space α] [baire_space α] [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} [topological_space α] [baire_space α] {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} [topological_space α] [baire_space α] {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} [topological_space α] [baire_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} [topological_space α] [baire_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_of_mem_residual {α : Type u_1} [topological_space α] [baire_space α] {s : set α} (hs : s residual α) :
@[protected, instance]
theorem is_Gδ.dense_Union_interior_of_closed {α : Type u_1} {ι : Type u_4} [topological_space α] [baire_space α] [encodable ι] {s : set α} (hs : is_Gδ s) (hd : dense s) {f : ι → set α} (hc : ∀ (i : ι), is_closed (f i)) (hU : s ⋃ (i : ι), f i) :
dense (⋃ (i : ι), interior (f i))

If a countable family of closed sets cover a dense set, then the union of their interiors is dense. Formulated here with .

theorem is_Gδ.dense_bUnion_interior_of_closed {α : Type u_1} {ι : Type u_4} [topological_space α] [baire_space α] {t : set ι} {s : set α} (hs : is_Gδ s) (hd : dense s) (ht : t.countable) {f : ι → set α} (hc : ∀ (i : ι), i tis_closed (f i)) (hU : s ⋃ (i : ι) (H : i t), f i) :
dense (⋃ (i : ι) (H : i t), interior (f i))

If a countable family of closed sets cover a dense set, then the union of their interiors is dense. Formulated here with a union over a countable set in any type.

theorem is_Gδ.dense_sUnion_interior_of_closed {α : Type u_1} [topological_space α] [baire_space α] {T : set (set α)} {s : set α} (hs : is_Gδ s) (hd : dense s) (hc : T.countable) (hc' : ∀ (t : set α), t Tis_closed t) (hU : s ⋃₀ T) :
dense (⋃ (t : set α) (H : t T), interior t)

If a countable family of closed sets cover a dense set, then the union of their interiors is dense. Formulated here with ⋃₀.

theorem dense_bUnion_interior_of_closed {α : Type u_1} {β : Type u_2} [topological_space α] [baire_space α] {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} [topological_space α] [baire_space α] {S : set (set α)} (hc : ∀ (s : set α), s Sis_closed 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} [topological_space α] [baire_space α] [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} [topological_space α] [baire_space α] [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.