Theorems · Definition · functional analysis

AddGroupNorm.casesOn

{G : Type u_6} →
  [inst : AddGroup G] →
    {motive : AddGroupNorm G → Sort u} →
      (t : AddGroupNorm G) →
        ((toAddGroupSeminorm : AddGroupSeminorm G) →
            (eq_zero_of_map_eq_zero' : ∀ (x : G), toAddGroupSeminorm.toFun x = 0 → x = 0) →
              motive { toAddGroupSeminorm := toAddGroupSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' }) →
          motive t

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

Realstatement · cited by 25,697
AddGroupstatement and proof · cited by 4,410
AddGroupSeminormstatement and proof · cited by 50
AddGroupSeminorm.toFunstatement and proof · cited by 47
AddGroupNormstatement and proof · cited by 16

Cited by2

Results whose statement or proof uses this declaration.

AddGroupNorm.noConfusionproof · cited by 0
AddGroupNorm.noConfusionTypeproof · cited by 0