Open covers #
We define IsOpenCover as a predicate on indexed families of open sets in a topological space X,
asserting that their union is X. This is an example of a declaration whose name is actually
longer than its content; but giving it a name serves as a way of standardizing API.
def
TopologicalSpace.IsOpenCover
{ι : Type u_1}
{X : Type u_2}
[TopologicalSpace X]
(u : ι → Opens X)
:
An indexed family of open sets whose union is X.
Equations
- TopologicalSpace.IsOpenCover u = (iSup u = ⊤)
Instances For
theorem
TopologicalSpace.IsOpenCover.mk
{ι : Type u_1}
{X : Type u_3}
[TopologicalSpace X]
{u : ι → Opens X}
(h : iSup u = ⊤)
:
theorem
TopologicalSpace.IsOpenCover.of_sets
{ι : Type u_1}
{X : Type u_3}
[TopologicalSpace X]
{v : ι → Set X}
(h_open : ∀ (i : ι), IsOpen (v i))
(h_iUnion : ⋃ (i : ι), v i = Set.univ)
:
IsOpenCover fun (i : ι) => { carrier := v i, is_open' := ⋯ }
theorem
TopologicalSpace.IsOpenCover.iSup_eq_top
{ι : Type u_1}
{X : Type u_3}
[TopologicalSpace X]
{u : ι → Opens X}
(hu : IsOpenCover u)
:
theorem
TopologicalSpace.IsOpenCover.iSup_set_eq_univ
{ι : Type u_1}
{X : Type u_3}
[TopologicalSpace X]
{u : ι → Opens X}
(hu : IsOpenCover u)
:
theorem
TopologicalSpace.IsOpenCover.comap
{κ : Type u_2}
{X : Type u_3}
{Y : Type u_4}
[TopologicalSpace X]
[TopologicalSpace Y]
{v : κ → Opens Y}
(hv : IsOpenCover v)
(f : C(X, Y))
:
IsOpenCover fun (k : κ) => (Opens.comap f) (v k)
Pullback of a covering of Y by a continuous map X → Y, giving a covering of X with the
same index type.
theorem
TopologicalSpace.IsOpenCover.exists_mem
{ι : Type u_1}
{X : Type u_3}
[TopologicalSpace X]
{u : ι → Opens X}
(hu : IsOpenCover u)
(a : X)
:
∃ (i : ι), a ∈ u i
theorem
TopologicalSpace.IsOpenCover.exists_mem_nhds
{ι : Type u_1}
{X : Type u_3}
[TopologicalSpace X]
{u : ι → Opens X}
(hu : IsOpenCover u)
(a : X)
:
theorem
TopologicalSpace.IsOpenCover.iUnion_inter
{ι : Type u_1}
{X : Type u_3}
[TopologicalSpace X]
{u : ι → Opens X}
(hu : IsOpenCover u)
(s : Set X)
: