{ι : Type u_5} →
  {B : Type u_6} →
    [inst : TopologicalSpace B] →
      {F : Type u_7} →
        [inst_1 : TopologicalSpace F] →
          (baseSet : ι → Set B) →
            (∀ (i : ι), IsOpen (baseSet i)) →
              (indexAt : B → ι) →
                (∀ (x : B), x ∈ baseSet (indexAt x)) →
                  (coordChange : ι → ι → B → F → F) →
                    (∀ (i : ι), ∀ x ∈ baseSet i, ∀ (v : F), coordChange i i x v = v) →
                      (∀ (i j : ι),
                          ContinuousOn (fun p => coordChange i j p.1 p.2) ((baseSet i ∩ baseSet j) ×ˢ Set.univ)) →
                        (∀ (i j k : ι),
                            ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k,
                              ∀ (v : F), coordChange j k x (coordChange i j x v) = coordChange i k x v) →
                          FiberBundleCore ι B F