apply_one — Mathlib

English

For x ∈ E, the unit NonarchAddGroupSeminorm evaluates to 0 at zero and to 1 otherwise: (1 : NonarchAddGroupSeminorm E) x = if x = 0 then 0 else 1.

Русский

Для x ∈ E единичный NonarchAddGroupSeminorm принимает значение 0 в нуле и 1 в остальных случаях: (1 : NonarchAddGroupSeminorm E) x = if x = 0 then 0 else 1.

LaTeX

$$$ (1 : \mathrm{NonarchAddGroupSeminorm}(E)) x = \begin{cases}0,& x=0\\ 1,& x\neq 0\end{cases} $$$

Lean4

@[simp]
theorem apply_one [DecidableEq E] (x : E) : (1 : NonarchAddGroupSeminorm E) x = if x = 0 then 0 else 1 :=
  rfl

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