Theorems · Definition · algebraic topology

Bundle.ContinuousRiemannianMetric.noConfusion

{P : Sort u} →
  {B : Type u_4} →
    {inst : TopologicalSpace B} →
      {F : Type u_5} →
        {inst_1 : NormedAddCommGroup F} →
          {inst_2 : NormedSpace ℝ F} →
            {E : B → Type u_6} →
              {inst_3 : TopologicalSpace (Bundle.TotalSpace F E)} →
                {inst_4 : (b : B) → TopologicalSpace (E b)} →
                  {inst_5 : (b : B) → AddCommGroup (E b)} →
                    {inst_6 : (b : B) → Module ℝ (E b)} →
                      {inst_7 : FiberBundle F E} →
                        {inst_8 : VectorBundle ℝ F E} →
                          {t : Bundle.ContinuousRiemannianMetric F E} →
                            {B' : Type u_4} →
                              {inst' : TopologicalSpace B'} →
                                {F' : Type u_5} →
                                  {inst'_1 : NormedAddCommGroup F'} →
                                    {inst'_2 : NormedSpace ℝ F'} →
                                      {E' : B' → Type u_6} →
                                        {inst'_3 : TopologicalSpace (Bundle.TotalSpace F' E')} →
                                          {inst'_4 : (b : B') → TopologicalSpace (E' b)} →
                                            {inst'_5 : (b : B') → AddCommGroup (E' b)} →
                                              {inst'_6 : (b : B') → Module ℝ (E' b)} →
                                                {inst'_7 : FiberBundle F' E'} →
                                                  {inst'_8 : VectorBundle ℝ F' E'} →
                                                    {t' : Bundle.ContinuousRiemannianMetric F' E'} →
                                                      B = B' →
                                                        inst ≍ inst' →
                                                          F = F' →
                                                            inst_1 ≍ inst'_1 →
                                                              inst_2 ≍ inst'_2 →
                                                                E ≍ E' →
                                                                  inst_3 ≍ inst'_3 →
                                                                    inst_4 ≍ inst'_4 →
                                                                      inst_5 ≍ inst'_5 →
                                                                        inst_6 ≍ inst'_6 →
                                                                          inst_7 ≍ inst'_7 →
                                                                            inst_8 ≍ inst'_8 →
                                                                              t ≍ t' →
                                                                                Bundle.ContinuousRiemannianMetric.noConfusionType
                                                                                  P t t'

Defined in

Mathlib.Topology.VectorBundle.Riemannian

Cited by

0 results in Mathlib

Foundations

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