Theorems · Inductive type · order theory

GroupSeminormClass

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

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

Defined in

Mathlib.Algebra.Order.Hom.Basic

Cited by

9 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

GroupAddCommMonoidPartialOrderFunLike