Theorems · Definition · functional analysis

NormedCommGroup.mk.noConfusion

{E : Type u_8} →
  {P : Sort u} →
    {toNorm : Norm E} →
      {toCommGroup : CommGroup E} →
        {toMetricSpace : MetricSpace E} →
          {dist_eq : autoParam (∀ (x y : E), dist x y = ‖x⁻¹ * y‖) NormedCommGroup.dist_eq._autoParam} →
            {toNorm' : Norm E} →
              {toCommGroup' : CommGroup E} →
                {toMetricSpace' : MetricSpace E} →
                  {dist_eq' : autoParam (∀ (x y : E), dist x y = ‖x⁻¹ * y‖) NormedCommGroup.dist_eq._autoParam} →
                    { toNorm := toNorm, toCommGroup := toCommGroup, toMetricSpace := toMetricSpace,
                          dist_eq := dist_eq } =
                        { toNorm := toNorm', toCommGroup := toCommGroup', toMetricSpace := toMetricSpace',
                          dist_eq := dist_eq' } →
                      (toNorm ≍ toNorm' → toCommGroup ≍ toCommGroup' → toMetricSpace ≍ toMetricSpace' → P) → P

Defined in

Mathlib.Analysis.Normed.Group.Defs

Cited by

0 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms