instZeroGroupSeminorm — Mathlib

English

There is a zero GroupSeminorm on E, given by the constant zero function, with map_one' holding trivially and the multiplication bound by zero.

Русский

Существует нулевой GroupSeminorm на E, задаваемый константной нулевой функцией; отображение единицы нулю соблюдается тривиально, а неравенство умножения обращено к нулю.

LaTeX

$$Zero (GroupSeminorm E)$$

Lean4

@[to_additive]
instance instZeroGroupSeminorm : Zero (GroupSeminorm E) :=
  ⟨{  toFun := 0
      map_one' := Pi.zero_apply _
      mul_le' := fun _ _ => (zero_add _).ge
      inv' := fun _ => rfl }⟩

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