English
There is a definition of infimum for seminorms via an iInf over a family of additive norms; it yields a seminorm.
Русский
Определение инфимума семинорм через iInf над семейством норм даёт новый семинорм.
LaTeX
$$new infimum construction via iInf: (p ⊓ q)(x) = ⨅ u (p(u) + q(x-u))$$
Lean4
noncomputable instance instLattice : Lattice (Seminorm 𝕜 E) :=
{ Seminorm.instSemilatticeSup with
inf := (· ⊓ ·)
inf_le_left := fun p q x => ciInf_le_of_le bddBelow_range_add x <| by simp only [sub_self, map_zero, add_zero]; rfl
inf_le_right := fun p q x => ciInf_le_of_le bddBelow_range_add 0 <| by simp only [map_zero, zero_add, sub_zero]; rfl
le_inf := fun a _ _ hab hac _ => le_ciInf fun _ => (le_map_add_map_sub a _ _).trans <| add_le_add (hab _) (hac _) }
