Theorems · Definition · functional analysis

ENormedAddCommMonoid.noConfusion

{P : Sort u} →
  {E : Type u_8} →
    {inst : TopologicalSpace E} →
      {t : ENormedAddCommMonoid E} →
        {E' : Type u_8} →
          {inst' : TopologicalSpace E'} →
            {t' : ENormedAddCommMonoid E'} →
              E = E' → inst ≍ inst' → t ≍ t' → ENormedAddCommMonoid.noConfusionType P t t'

Defined in: Mathlib.Analysis.Normed.Group.Defs
Cited by: 0 results in Mathlib
Foundations: Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
ENorm.enormproof · cited by 715
ENormedAddCommMonoidstatement and proof · cited by 32
ESeminormedAddCommMonoidproof · cited by 21
ENormedAddCommMonoid.noConfusionTypestatement · cited by 0
ENormedAddCommMonoid.casesOnproof · cited by 0

Cited by1

Results whose statement or proof uses this declaration.

ENormedAddCommMonoid.mk.noConfusionproof · cited by 0