English
The infimum operation makes Seminorm a lattice: it preserves scalar action and subadditivity under convolution.
Русский
Операция инфимум образует мн-во полупорядоченное под полином; сохраняет скалярное действие и субаддитивность через свёртку.
LaTeX
$$...$$
Lean4
noncomputable instance instInf : Min (Seminorm 𝕜 E) where
min p
q :=
{
p.toAddGroupSeminorm ⊓
q.toAddGroupSeminorm with
toFun := fun x => ⨅ u : E, p u + q (x - u)
smul' := by
intro a x
obtain rfl | ha := eq_or_ne a 0
· rw [norm_zero, zero_mul, zero_smul]
refine
ciInf_eq_of_forall_ge_of_forall_gt_exists_lt (fun i => by positivity) fun x hx =>
⟨0, by rwa [map_zero, sub_zero, map_zero, add_zero]⟩
simp_rw [Real.mul_iInf_of_nonneg (norm_nonneg a), mul_add, ← map_smul_eq_mul p, ← map_smul_eq_mul q, smul_sub]
refine Function.Surjective.iInf_congr ((a⁻¹ • ·) : E → E) (fun u => ⟨a • u, inv_smul_smul₀ ha u⟩) fun u => ?_
rw [smul_inv_smul₀ ha] }
