Mathlib Map

Theorems · Inductive type · functional analysis

SeminormClass

(F : Type u_12) →
  (𝕜 : outParam (Type u_13)) →
    (E : outParam (Type u_14)) → [SeminormedRing 𝕜] → [AddGroup E] → [SMul 𝕜 E] → [FunLike F E ℝ] → Prop

SeminormClass F 𝕜 E states that F is a type of seminorms on the 𝕜-module E. You should extend this class when you extend Seminorm.

Defined in
Mathlib.Analysis.Seminorm
Cited by
1 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
SeminormedRingAddGroupSMulFunLike
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SeminormClass.map_smul_eq_mul · cited by 25SeminormClass.map_smul_eq…SeminormClass.casesOn · cited by 0SeminormClass.casesOnSeminormClass.recOn · cited by 0SeminormClass.recOnReal · cited by 25697RealAddGroup · cited by 4410AddGroupFunLike · cited by 2560FunLikeSeminormedRing · cited by 446SeminormedRingSeminormClassCITED BYCITES

Cites4

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

Cited by3

Results whose statement or proof uses this declaration.