Theorems · Definition · order theory

AddGroupSeminormClass.casesOn

{F : Type u_7} →
  {α : Type u_8} →
    {β : Type u_9} →
      [inst : AddGroup α] →
        [inst_1 : AddCommMonoid β] →
          [inst_2 : PartialOrder β] →
            [inst_3 : FunLike F α β] →
              {motive : AddGroupSeminormClass F α β → Sort u} →
                (t : AddGroupSeminormClass F α β) →
                  ([toSubadditiveHomClass : SubadditiveHomClass F α β] →
                      (map_zero : ∀ (f : F), f 0 = 0) → (map_neg_eq_map : ∀ (f : F) (a : α), f (-a) = f a) → motive ⋯) →
                    motive t

Defined in

Mathlib.Algebra.Order.Hom.Basic

Cited by

0 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext

Assumes

AddGroupAddCommMonoidPartialOrderFunLike