groupSeminormClass — Mathlib

English

There exists a GroupSeminormClass structure on GroupSeminorm E with evaluation to E, Real-valued; the axioms include map_one_eq_zero, map_mul_le_add, map_inv_eq_map.

Русский

Существует структура GroupSeminormClass на GroupSeminorm E с отображением в E, ℝ; аксиомы: map_one_eq_zero, map_mul_le_add, map_inv_eq_map.

LaTeX

$$\\text{GroupSeminormClass } (GroupSeminorm E) E \\mathbb{R} \\text{ with } map_one_eq_zero, map_mul_le_add, map_inv_eq_map$$

Lean4

@[to_additive]
instance groupSeminormClass : GroupSeminormClass (GroupSeminorm E) E ℝ
    where
  map_one_eq_zero f := f.map_one'
  map_mul_le_add f := f.mul_le'
  map_inv_eq_map f := f.inv'

Похожие утверждения