English
The lattice structure on GroupSeminorm E is provided by the semilatticeSup; backward and forward equations characterize inf and sup with respect to pointwise operations.
Русский
У GroupSeminorm E есть решетка, задаваемая через semilatticeSup; определяются inf и sup по точкам.
LaTeX
$$$\text{GroupSeminorm}(E) \text{ is a lattice with } \inf(p,q) = p \sqcap q,\; \sup(p,q) = p \sqcup q,$ где $ (p \sqcup q)(x) = p(x) \sqcup q(x).$$$
Lean4
@[to_additive]
noncomputable instance : Lattice (GroupSeminorm E) :=
{ GroupSeminorm.semilatticeSup with
inf := (· ⊓ ·)
inf_le_left := fun p q x =>
ciInf_le_of_le mul_bddBelow_range_add x <| by rw [div_self', map_one_eq_zero q, add_zero]
inf_le_right := fun p q x =>
ciInf_le_of_le mul_bddBelow_range_add (1 : E) <| by
simpa only [div_one x, map_one_eq_zero p, zero_add (q x)] using le_rfl
le_inf := fun a _ _ hb hc _ => le_ciInf fun _ => (le_map_add_map_div a _ _).trans <| add_le_add (hb _) (hc _) }
