mathlib3 documentation

topology.metric_space.baire

Baire theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]

structure baire_space (α : Type u_5) [topological_space α] :

Prop

baire_property : ∀ (f : ℕ → set α), (∀ (n : ℕ), is_open (f n)) → (∀ (n : ℕ), dense (f n)) → dense (⋂ (n : ℕ), f n)

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]

def baire_category_theorem_emetric_complete {α : Type u_1} [pseudo_emetric_space α] [complete_space α] :

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]

def baire_category_theorem_locally_compact {α : Type u_1} [topological_space α] [t2_space α] [locally_compact_space α] :

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 ∈ S → is_open s) (hS : S.countable) (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_bInter_of_open {α : Type u_1} {β : Type u_2} [topological_space α] [baire_space α] {S : set β} {f : β → set α} (ho : ∀ (s : β), s ∈ S → is_open (f s)) (hS : S.countable) (hd : ∀ (s : β), s ∈ S → dense (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 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 Gδ set.

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 ∈ 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} [topological_space α] [baire_space α] {s : set α} (hs : s ∈ residual α) :

theorem dense_sInter_of_Gδ {α : Type u_1} [topological_space α] [baire_space α] {S : set (set α)} (ho : ∀ (s : set α), s ∈ S → is_Gδ s) (hS : S.countable) (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_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 ∈ S → set α} (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 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 Gδ 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 ∈ t → is_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 Gδ 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 ∈ T → is_closed t) (hU : s ⊆ ⋃₀ T) :

dense (⋃ (t : set α) (H : 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_bUnion_interior_of_closed {α : Type u_1} {β : Type u_2} [topological_space α] [baire_space α] {S : set β} {f : β → set α} (hc : ∀ (s : β), s ∈ S → is_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 ∈ S → is_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.