Theorems · Definition · algebraic topology

VectorPrebundle.mk.noConfusion

{R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        {inst : NontriviallyNormedField R} →
          {inst_1 : (x : B) → AddCommMonoid (E x)} →
            {inst_2 : (x : B) → Module R (E x)} →
              {inst_3 : NormedAddCommGroup F} →
                {inst_4 : NormedSpace R F} →
                  {inst_5 : TopologicalSpace B} →
                    {inst_6 : (x : B) → TopologicalSpace (E x)} →
                      {P : Sort u} →
                        {pretrivializationAtlas : Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj)} →
                          {pretrivialization_linear' :
                              ∀ e ∈ pretrivializationAtlas, Bundle.Pretrivialization.IsLinear R e} →
                            {pretrivializationAt : B → Bundle.Pretrivialization F Bundle.TotalSpace.proj} →
                              {mem_base_pretrivializationAt : ∀ (x : B), x ∈ (pretrivializationAt x).baseSet} →
                                {pretrivialization_mem_atlas :
                                    ∀ (x : B), pretrivializationAt x ∈ pretrivializationAtlas} →
                                  {exists_coordChange :
                                      ∀ e ∈ pretrivializationAtlas,
                                        ∀ e' ∈ pretrivializationAtlas,
                                          ∃ f,
                                            ContinuousOn f (e.baseSet ∩ e'.baseSet) ∧
                                              ∀ b ∈ e.baseSet ∩ e'.baseSet,
                                                ∀ (v : F), (f b) v = (↑e' ⟨b, e.symm b v⟩).2} →
                                    {totalSpaceMk_isInducing :
                                        ∀ (b : B),
                                          Topology.IsInducing (↑(pretrivializationAt b) ∘ Bundle.TotalSpace.mk b)} →
                                      {pretrivializationAtlas' :
                                          Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj)} →
                                        {pretrivialization_linear'' :
                                            ∀ e ∈ pretrivializationAtlas', Bundle.Pretrivialization.IsLinear R e} →
                                          {pretrivializationAt' :
                                              B → Bundle.Pretrivialization F Bundle.TotalSpace.proj} →
                                            {mem_base_pretrivializationAt' :
                                                ∀ (x : B), x ∈ (pretrivializationAt' x).baseSet} →
                                              {pretrivialization_mem_atlas' :
                                                  ∀ (x : B), pretrivializationAt' x ∈ pretrivializationAtlas'} →
                                                {exists_coordChange' :
                                                    ∀ e ∈ pretrivializationAtlas',
                                                      ∀ e' ∈ pretrivializationAtlas',
                                                        ∃ f,
                                                          ContinuousOn f (e.baseSet ∩ e'.baseSet) ∧
                                                            ∀ b ∈ e.baseSet ∩ e'.baseSet,
                                                              ∀ (v : F), (f b) v = (↑e' ⟨b, e.symm b v⟩).2} →
                                                  {totalSpaceMk_isInducing' :
                                                      ∀ (b : B),
                                                        Topology.IsInducing
                                                          (↑(pretrivializationAt' b) ∘ Bundle.TotalSpace.mk b)} →
                                                    { pretrivializationAtlas := pretrivializationAtlas,
                                                          pretrivialization_linear' := pretrivialization_linear',
                                                          pretrivializationAt := pretrivializationAt,
                                                          mem_base_pretrivializationAt := mem_base_pretrivializationAt,
                                                          pretrivialization_mem_atlas := pretrivialization_mem_atlas,
                                                          exists_coordChange := exists_coordChange,
                                                          totalSpaceMk_isInducing := totalSpaceMk_isInducing } =
                                                        { pretrivializationAtlas := pretrivializationAtlas',
                                                          pretrivialization_linear' := pretrivialization_linear'',
                                                          pretrivializationAt := pretrivializationAt',
                                                          mem_base_pretrivializationAt := mem_base_pretrivializationAt',
                                                          pretrivialization_mem_atlas := pretrivialization_mem_atlas',
                                                          exists_coordChange := exists_coordChange',
                                                          totalSpaceMk_isInducing := totalSpaceMk_isInducing' } →
                                                      (pretrivializationAtlas ≍ pretrivializationAtlas' →
                                                          pretrivializationAt ≍ pretrivializationAt' → P) →
                                                        P

Defined in

Mathlib.Topology.VectorBundle.Basic

Cited by

1 results in Mathlib

Foundations

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