Theorems · Inductive type · order theory

AddGroupSeminormClass

(F : Type u_7) →
  (α : outParam (Type u_8)) →
    (β : outParam (Type u_9)) → [AddGroup α] → [AddCommMonoid β] → [PartialOrder β] → [FunLike F α β] → Prop

AddGroupSeminormClass F α states that F is a type of β-valued seminorms on the additive group α. You should extend this class when you extend AddGroupSeminorm.

Defined in

Mathlib.Algebra.Order.Hom.Basic

Cited by

18 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

AddGroupAddCommMonoidPartialOrderFunLike