Theorems · Definition · functional analysis

HilbertBasis.noConfusion

{P : Sort u} →
  {ι : Type u_1} →
    {𝕜 : Type u_2} →
      {inst : RCLike 𝕜} →
        {E : Type u_3} →
          {inst_1 : NormedAddCommGroup E} →
            {inst_2 : InnerProductSpace 𝕜 E} →
              {t : HilbertBasis ι 𝕜 E} →
                {ι' : Type u_1} →
                  {𝕜' : Type u_2} →
                    {inst' : RCLike 𝕜'} →
                      {E' : Type u_3} →
                        {inst'_1 : NormedAddCommGroup E'} →
                          {inst'_2 : InnerProductSpace 𝕜' E'} →
                            {t' : HilbertBasis ι' 𝕜' E'} →
                              ι = ι' →
                                𝕜 = 𝕜' →
                                  inst ≍ inst' →
                                    E = E' →
                                      inst_1 ≍ inst'_1 → inst_2 ≍ inst'_2 → t ≍ t' → HilbertBasis.noConfusionType P t t'

Defined in

Mathlib.Analysis.InnerProductSpace.l2Space

Cited by

0 results in Mathlib

Foundations

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