toOne — Mathlib

English

Equational characterizations identify the lattice structure with the semilatticeSup-based definitions.

Русский

Эквивалентности описывают структуру решетки через определения на основе ⊔.

LaTeX

$$$\text{GroupSeminorm}_{\text{eq}}(E) = \text{GroupSeminorm}_{\text{lattice}}(E).$$$

Lean4

instance toOne [DecidableEq E] : One (AddGroupSeminorm E) :=
  ⟨{  toFun := fun x => if x = 0 then 0 else 1
      map_zero' := if_pos rfl
      add_le' := fun x y => by
        by_cases hx : x = 0
        · rw [if_pos hx, hx, zero_add, zero_add]
        · rw [if_neg hx]
          refine le_add_of_le_of_nonneg ?_ ?_ <;> split_ifs <;> norm_num
      neg' := fun x => by simp_rw [neg_eq_zero] }⟩

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