English
There exists a distinguished One element in GroupSeminorm E, given by the function toFun x = if x = 1 then 0 else 1, with the usual properties of a seminorm.
Русский
Существует особый элемент One в GroupSeminorm E, задаваемый функцией toFun x = если x = 1, то 0, иначе 1, обладающий обычными свойствами семинорма.
LaTeX
$$$ (1 : \mathrm{GroupSeminorm}(E))(x) = \begin{cases}0,& x=1\\ 1,& x\neq 1\end{cases} $$$
Lean4
instance toOne [DecidableEq E] : One (GroupSeminorm E) :=
⟨{ toFun := fun x => if x = 1 then 0 else 1
map_one' := if_pos rfl
mul_le' := fun x y => by
by_cases hx : x = 1
· rw [if_pos hx, hx, one_mul, zero_add]
· rw [if_neg hx]
refine le_add_of_le_of_nonneg ?_ ?_ <;> split_ifs <;> norm_num
inv' := fun x => by simp_rw [inv_eq_one] }⟩
