Documentation

Mathlib.Topology.ShrinkingLemma

The shrinking lemma #

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

theorem ShrinkingLemma.PartialRefinement.ext {ι : Type u_1} {X : Type u_2} :
∀ {inst : TopologicalSpace X} {u : ιSet X} {s : Set X} {x y : ShrinkingLemma.PartialRefinement u s}, x.toFun = y.toFunx.carrier = y.carrierx = y
theorem ShrinkingLemma.PartialRefinement.ext_iff {ι : Type u_1} {X : Type u_2} :
∀ {inst : TopologicalSpace X} {u : ιSet X} {s : Set X} {x y : ShrinkingLemma.PartialRefinement u s}, x = y x.toFun = y.toFun x.carrier = y.carrier
structure ShrinkingLemma.PartialRefinement {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] (u : ιSet X) (s : Set X) :
Type (max u_1 u_2)

Auxiliary definition for the proof of the 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 following 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.

  • toFun : ιSet X

    A family of sets that form a partial refinement of u.

  • carrier : Set ι

    The set of indexes i such that i-th set is already shrunk.

  • isOpen : ∀ (i : ι), IsOpen (self.toFun i)

    Each set from the partially refined family is open.

  • subset_iUnion : s ⋃ (i : ι), self.toFun i

    The partially refined family still covers the set.

  • closure_subset : ∀ {i : ι}, i self.carrierclosure (self.toFun i) u i

    For each i ∈ carrier, the original set includes the closure of the refined set.

  • apply_eq : ∀ {i : ι}, iself.carrierself.toFun i = u i

    Sets that correspond to i ∉ carrier are not modified.

Instances For
    theorem ShrinkingLemma.PartialRefinement.isOpen {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} {s : Set X} (self : ShrinkingLemma.PartialRefinement u s) (i : ι) :
    IsOpen (self.toFun i)

    Each set from the partially refined family is open.

    theorem ShrinkingLemma.PartialRefinement.subset_iUnion {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} {s : Set X} (self : ShrinkingLemma.PartialRefinement u s) :
    s ⋃ (i : ι), self.toFun i

    The partially refined family still covers the set.

    theorem ShrinkingLemma.PartialRefinement.closure_subset {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} {s : Set X} (self : ShrinkingLemma.PartialRefinement u s) {i : ι} :
    i self.carrierclosure (self.toFun i) u i

    For each i ∈ carrier, the original set includes the closure of the refined set.

    theorem ShrinkingLemma.PartialRefinement.apply_eq {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} {s : Set X} (self : ShrinkingLemma.PartialRefinement u s) {i : ι} :
    iself.carrierself.toFun i = u i

    Sets that correspond to i ∉ carrier are not modified.

    Equations
    • ShrinkingLemma.PartialRefinement.instCoeFunForallSet = { coe := ShrinkingLemma.PartialRefinement.toFun }
    theorem ShrinkingLemma.PartialRefinement.subset {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} {s : Set X} (v : ShrinkingLemma.PartialRefinement u s) (i : ι) :
    v.toFun i u i
    Equations
    theorem ShrinkingLemma.PartialRefinement.apply_eq_of_chain {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} {s : Set X} {c : Set (ShrinkingLemma.PartialRefinement u s)} (hc : IsChain (fun (x1 x2 : ShrinkingLemma.PartialRefinement u s) => x1 x2) c) {v₁ : ShrinkingLemma.PartialRefinement u s} {v₂ : ShrinkingLemma.PartialRefinement u s} (h₁ : v₁ c) (h₂ : v₂ c) {i : ι} (hi₁ : i v₁.carrier) (hi₂ : i v₂.carrier) :
    v₁.toFun i = v₂.toFun 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.

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

    Equations
    Instances For
      def ShrinkingLemma.PartialRefinement.find {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} {s : Set X} (c : Set (ShrinkingLemma.PartialRefinement u s)) (ne : c.Nonempty) (i : ι) :

      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
      Instances For
        theorem ShrinkingLemma.PartialRefinement.find_mem {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} {s : Set X} {c : Set (ShrinkingLemma.PartialRefinement u s)} (i : ι) (ne : c.Nonempty) :
        theorem ShrinkingLemma.PartialRefinement.find_apply_of_mem {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} {s : Set X} {c : Set (ShrinkingLemma.PartialRefinement u s)} (hc : IsChain (fun (x1 x2 : ShrinkingLemma.PartialRefinement u s) => x1 x2) c) (ne : c.Nonempty) {i : ι} {v : ShrinkingLemma.PartialRefinement u s} (hv : v c) (hi : i v.carrier) :
        (ShrinkingLemma.PartialRefinement.find c ne i).toFun i = v.toFun i
        def ShrinkingLemma.PartialRefinement.chainSup {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} {s : Set X} (c : Set (ShrinkingLemma.PartialRefinement u s)) (hc : IsChain (fun (x1 x2 : ShrinkingLemma.PartialRefinement u s) => x1 x2) c) (ne : c.Nonempty) (hfin : xs, {i : ι | x u i}.Finite) (hU : s ⋃ (i : ι), u i) :

        Least upper bound of a nonempty chain of partial refinements.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem ShrinkingLemma.PartialRefinement.le_chainSup {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} {s : Set X} {c : Set (ShrinkingLemma.PartialRefinement u s)} (hc : IsChain (fun (x1 x2 : ShrinkingLemma.PartialRefinement u s) => x1 x2) c) (ne : c.Nonempty) (hfin : xs, {i : ι | x u i}.Finite) (hU : s ⋃ (i : ι), u i) {v : ShrinkingLemma.PartialRefinement u s} (hv : v c) :

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

          theorem ShrinkingLemma.PartialRefinement.exists_gt {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} {s : Set X} [NormalSpace X] (v : ShrinkingLemma.PartialRefinement u s) (hs : IsClosed s) (i : ι) (hi : iv.carrier) :
          ∃ (v' : ShrinkingLemma.PartialRefinement 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.

          theorem exists_subset_iUnion_closure_subset {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} {s : Set X} [NormalSpace X] (hs : IsClosed s) (uo : ∀ (i : ι), IsOpen (u i)) (uf : xs, {i : ι | x u i}.Finite) (us : s ⋃ (i : ι), u i) :
          ∃ (v : ιSet X), s Set.iUnion v (∀ (i : ι), IsOpen (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.

          theorem exists_subset_iUnion_closed_subset {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} {s : Set X} [NormalSpace X] (hs : IsClosed s) (uo : ∀ (i : ι), IsOpen (u i)) (uf : xs, {i : ι | x u i}.Finite) (us : s ⋃ (i : ι), u i) :
          ∃ (v : ιSet X), s Set.iUnion v (∀ (i : ι), IsClosed (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_iUnion_closure_subset for a stronger statement.

          theorem exists_iUnion_eq_closure_subset {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} [NormalSpace X] (uo : ∀ (i : ι), IsOpen (u i)) (uf : ∀ (x : X), {i : ι | x u i}.Finite) (uU : ⋃ (i : ι), u i = Set.univ) :
          ∃ (v : ιSet X), Set.iUnion v = Set.univ (∀ (i : ι), IsOpen (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.

          theorem exists_iUnion_eq_closed_subset {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ιSet X} [NormalSpace X] (uo : ∀ (i : ι), IsOpen (u i)) (uf : ∀ (x : X), {i : ι | x u i}.Finite) (uU : ⋃ (i : ι), u i = Set.univ) :
          ∃ (v : ιSet X), Set.iUnion v = Set.univ (∀ (i : ι), IsClosed (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_iUnion_eq_closure_subset for a stronger statement.