apply_one — Mathlib

English

For x ∈ E, the unit seminorm takes the value 0 at the identity and 1 otherwise: (1 : GroupSeminorm E) x = if x = 1 then 0 else 1.

Русский

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

LaTeX

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

Lean4

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

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