mathlib3 documentation

topology.shrinking_lemma

The shrinking lemma #

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

In this file we prove a few versions of the shrinking lemma. The lemma says that in a normal topological space a point finite open covering can be “shrunk”: for a point finite open covering u : ι → set X there exists a refinement v : ι → set X such that closure (v i) ⊆ u i.

For finite or countable coverings this lemma can be proved without the axiom of choice, see ncatlab for details. We only formalize the most general result that works for any covering but needs the axiom of choice.

We prove two versions of the lemma:

Tags #

normal space, shrinking lemma

source
@[nolint, ext]
structure shrinking_lemma.partial_refinement {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] (u : ι → set X) (s : set X) :
Type (max u_1 u_2)

Auxiliary definition for the proof of shrinking_lemma. A partial refinement of a covering ⋃ i, u i of a set s is a map v : ι → set X and a set carrier : set ι such that

  • s ⊆ ⋃ i, v i;
  • all v i are open;
  • if i ∈ carrier v, then closure (v i) ⊆ u i;
  • if i ∉ carrier, then v i = u i.

This type is equipped with the folowing partial order: v ≤ v' if v.carrier ⊆ v'.carrier and v i = v' i for i ∈ v.carrier. We will use Zorn's lemma to prove that this type has a maximal element, then show that the maximal element must have carrier = univ.

Instances for shrinking_lemma.partial_refinement
source
@[protected, instance]
def shrinking_lemma.partial_refinement.has_coe_to_fun {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} :
has_coe_to_fun (shrinking_lemma.partial_refinement u s) (λ (_x : shrinking_lemma.partial_refinement u s), ι → set X)
Equations
source
theorem shrinking_lemma.partial_refinement.subset_Union {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} (v : shrinking_lemma.partial_refinement u s) :
s ⊆ ⋃ (i : ι), ⇑v i
source
theorem shrinking_lemma.partial_refinement.closure_subset {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} (v : shrinking_lemma.partial_refinement u s) {i : ι} (hi : i ∈ v.carrier) :
closure (⇑v i) ⊆ u i
source
theorem shrinking_lemma.partial_refinement.apply_eq {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} (v : shrinking_lemma.partial_refinement u s) {i : ι} (hi : i ∉ v.carrier) :
⇑v i = u i
source
@[protected]
theorem shrinking_lemma.partial_refinement.is_open {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} (v : shrinking_lemma.partial_refinement u s) (i : ι) :
is_open (⇑v i)
source
@[protected]
theorem shrinking_lemma.partial_refinement.subset {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} (v : shrinking_lemma.partial_refinement u s) (i : ι) :
⇑v i ⊆ u i
source
theorem shrinking_lemma.partial_refinement.ext {ι : Type u_1} {X : Type u_2} {_inst_1 : topological_space X} {_inst_2 : normal_space X} {u : ι → set X} {s : set X} (x y : shrinking_lemma.partial_refinement u s) (h : x.to_fun = y.to_fun) (h_1 : x.carrier = y.carrier) :
x = y
source
theorem shrinking_lemma.partial_refinement.ext_iff {ι : Type u_1} {X : Type u_2} {_inst_1 : topological_space X} {_inst_2 : normal_space X} {u : ι → set X} {s : set X} (x y : shrinking_lemma.partial_refinement u s) :
x = y ↔ x.to_fun = y.to_fun ∧ x.carrier = y.carrier
source
@[protected, instance]
def shrinking_lemma.partial_refinement.partial_order {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} :
partial_order (shrinking_lemma.partial_refinement u s)
Equations
source
theorem shrinking_lemma.partial_refinement.apply_eq_of_chain {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} {c : set (shrinking_lemma.partial_refinement u s)} (hc : is_chain has_le.le c) {v₁ v₂ : shrinking_lemma.partial_refinement u s} (h₁ : v₁ ∈ c) (h₂ : v₂ ∈ c) {i : ι} (hi₁ : i ∈ v₁.carrier) (hi₂ : i ∈ v₂.carrier) :
⇑v₁ i = ⇑v₂ i

If two partial refinements v₁, v₂ belong to a chain (hence, they are comparable) and i belongs to the carriers of both partial refinements, then v₁ i = v₂ i.

source
def shrinking_lemma.partial_refinement.chain_Sup_carrier {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} (c : set (shrinking_lemma.partial_refinement u s)) :
set ι

The carrier of the least upper bound of a non-empty chain of partial refinements is the union of their carriers.

Equations
source
noncomputable def shrinking_lemma.partial_refinement.find {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} (c : set (shrinking_lemma.partial_refinement u s)) (ne : c.nonempty) (i : ι) :
shrinking_lemma.partial_refinement u s

Choice of an element of a nonempty chain of partial refinements. If i belongs to one of carrier v, v ∈ c, then find c ne i is one of these partial refinements.

Equations
source
theorem shrinking_lemma.partial_refinement.find_mem {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} {c : set (shrinking_lemma.partial_refinement u s)} (i : ι) (ne : c.nonempty) :
shrinking_lemma.partial_refinement.find c ne i ∈ c
source
theorem shrinking_lemma.partial_refinement.mem_find_carrier_iff {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} {c : set (shrinking_lemma.partial_refinement u s)} {i : ι} (ne : c.nonempty) :
i ∈ (shrinking_lemma.partial_refinement.find c ne i).carrier ↔ i ∈ shrinking_lemma.partial_refinement.chain_Sup_carrier c
source
theorem shrinking_lemma.partial_refinement.find_apply_of_mem {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} {c : set (shrinking_lemma.partial_refinement u s)} (hc : is_chain has_le.le c) (ne : c.nonempty) {i : ι} {v : shrinking_lemma.partial_refinement u s} (hv : v ∈ c) (hi : i ∈ v.carrier) :
⇑(shrinking_lemma.partial_refinement.find c ne i) i = ⇑v i
source
def shrinking_lemma.partial_refinement.chain_Sup {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} (c : set (shrinking_lemma.partial_refinement u s)) (hc : is_chain has_le.le c) (ne : c.nonempty) (hfin : ∀ (x : X), x ∈ s → {i : ι | x ∈ u i}.finite) (hU : s ⊆ ⋃ (i : ι), u i) :
shrinking_lemma.partial_refinement u s

Least upper bound of a nonempty chain of partial refinements.

Equations
source
theorem shrinking_lemma.partial_refinement.le_chain_Sup {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} {c : set (shrinking_lemma.partial_refinement u s)} (hc : is_chain has_le.le c) (ne : c.nonempty) (hfin : ∀ (x : X), x ∈ s → {i : ι | x ∈ u i}.finite) (hU : s ⊆ ⋃ (i : ι), u i) {v : shrinking_lemma.partial_refinement u s} (hv : v ∈ c) :
v ≤ shrinking_lemma.partial_refinement.chain_Sup c hc ne hfin hU

chain_Sup hu c hc ne hfin hU is an upper bound of the chain c.

source
theorem shrinking_lemma.partial_refinement.exists_gt {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} (v : shrinking_lemma.partial_refinement u s) (hs : is_closed s) (i : ι) (hi : i ∉ v.carrier) :
∃ (v' : shrinking_lemma.partial_refinement u s), v < v'

If s is a closed set, v is a partial refinement, and i is an index such that i ∉ v.carrier, then there exists a partial refinement that is strictly greater than v.

source
theorem exists_subset_Union_closure_subset {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} (hs : is_closed s) (uo : ∀ (i : ι), is_open (u i)) (uf : ∀ (x : X), x ∈ s → {i : ι | x ∈ u i}.finite) (us : s ⊆ ⋃ (i : ι), u i) :
∃ (v : ι → set X), s ⊆ set.Union v ∧ (∀ (i : ι), is_open (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i

Shrinking lemma. A point-finite open cover of a closed subset of a normal space can be "shrunk" to a new open cover so that the closure of each new open set is contained in the corresponding original open set.

source
theorem exists_subset_Union_closed_subset {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} {s : set X} (hs : is_closed s) (uo : ∀ (i : ι), is_open (u i)) (uf : ∀ (x : X), x ∈ s → {i : ι | x ∈ u i}.finite) (us : s ⊆ ⋃ (i : ι), u i) :
∃ (v : ι → set X), s ⊆ set.Union v ∧ (∀ (i : ι), is_closed (v i)) ∧ ∀ (i : ι), v i ⊆ u i

Shrinking lemma. A point-finite open cover of a closed subset of a normal space can be "shrunk" to a new closed cover so that each new closed set is contained in the corresponding original open set. See also exists_subset_Union_closure_subset for a stronger statement.

source
theorem exists_Union_eq_closure_subset {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} (uo : ∀ (i : ι), is_open (u i)) (uf : ∀ (x : X), {i : ι | x ∈ u i}.finite) (uU : (⋃ (i : ι), u i) = set.univ) :
∃ (v : ι → set X), set.Union v = set.univ ∧ (∀ (i : ι), is_open (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i

Shrinking lemma. A point-finite open cover of a closed subset of a normal space can be "shrunk" to a new open cover so that the closure of each new open set is contained in the corresponding original open set.

source
theorem exists_Union_eq_closed_subset {ι : Type u_1} {X : Type u_2} [topological_space X] [normal_space X] {u : ι → set X} (uo : ∀ (i : ι), is_open (u i)) (uf : ∀ (x : X), {i : ι | x ∈ u i}.finite) (uU : (⋃ (i : ι), u i) = set.univ) :
∃ (v : ι → set X), set.Union v = set.univ ∧ (∀ (i : ι), is_closed (v i)) ∧ ∀ (i : ι), v i ⊆ u i

Shrinking lemma. A point-finite open cover of a closed subset of a normal space can be "shrunk" to a new closed cover so that each of the new closed sets is contained in the corresponding original open set. See also exists_Union_eq_closure_subset for a stronger statement.