Theorems · Inductive type · general topology

ShrinkingLemma.PartialRefinement

{ι : Type u_1} → {X : Type u_2} → [TopologicalSpace X] → (ι → Set X) → Set X → (Set X → Prop) → 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.

Defined in

Mathlib.Topology.ShrinkingLemma

Cited by

21 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpace