Theorems · Definition · algebraic topology

IsOpen.trivializationDiscrete

{E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {f : E → X} →
          [Nonempty (X → E)] →
            {ι : Type u_3} →
              [Nonempty ι] →
                [inst_4 : TopologicalSpace ι] →
                  [DiscreteTopology ι] →
                    (U : ι → Set E) →
                      (V : Set X) →
                        IsOpen V →
                          (∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen W ↔ IsOpen (f ⁻¹' W ∩ U i))) →
                            (∀ (i : ι), Set.InjOn f (U i)) →
                              (∀ (i : ι), Set.SurjOn f (U i) V) →
                                Pairwise (Function.onFun Disjoint U) → f ⁻¹' V ⊆ ⋃ i, U i → Bundle.Trivialization ι f

Let f : E → X be a (not necessarily continuous) map between topological spaces, and let V be an open subset of X. Suppose that there is a family U of disjoint subsets of E that covers f⁻¹(V) such that for every i, 1. f is injective on Uᵢ, 2. V is contained in the image f(Uᵢ), 3. the open sets in V are determined by their preimages in Uᵢ. Then f admits a Bundle.Trivialization over the base set V.

Defined in

Mathlib.Topology.Covering.Basic

Cited by

3 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceNonemptyNonemptyTopologicalSpaceDiscreteTopology