Theorems · Definition · functional analysis

ENormedAddCommMonoid.mk.noConfusion

{E : Type u_8} →
  {inst : TopologicalSpace E} →
    {P : Sort u} →
      {toESeminormedAddCommMonoid : ESeminormedAddCommMonoid E} →
        {enorm_eq_zero : ∀ (x : E), ‖x‖ₑ = 0 ↔ x = 0} →
          {toESeminormedAddCommMonoid' : ESeminormedAddCommMonoid E} →
            {enorm_eq_zero' : ∀ (x : E), ‖x‖ₑ = 0 ↔ x = 0} →
              { toESeminormedAddCommMonoid := toESeminormedAddCommMonoid, enorm_eq_zero := enorm_eq_zero } =
                  { toESeminormedAddCommMonoid := toESeminormedAddCommMonoid', enorm_eq_zero := enorm_eq_zero' } →
                (toESeminormedAddCommMonoid ≍ toESeminormedAddCommMonoid' → P) → P

Defined in

Mathlib.Analysis.Normed.Group.Defs

Cited by

0 results in Mathlib

Foundations

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