English
ENormedSpace carries a SemilatticeSup structure via pointwise maximum of norms.
Русский
ENormedSpace обладает структурой SemilatticeSup через покомпонентную операцию максимум.
LaTeX
$$instance : SemilatticeSup (ENormedSpace 𝕜 V) := ...$$
Lean4
noncomputable instance : SemilatticeSup (ENormedSpace 𝕜 V) :=
{ ENormedSpace.partialOrder with
le := (· ≤ ·)
lt := (· < ·)
sup := fun e₁ e₂ =>
{ toFun := fun x => max (e₁ x) (e₂ x)
eq_zero' := fun _ h => e₁.eq_zero_iff.1 (ENNReal.max_eq_zero_iff.1 h).1
map_add_le' := fun _ _ =>
max_le (le_trans (e₁.map_add_le _ _) <| add_le_add (le_max_left _ _) (le_max_left _ _))
(le_trans (e₂.map_add_le _ _) <| add_le_add (le_max_right _ _) (le_max_right _ _))
map_smul_le' := fun c x => le_of_eq <| by simp only [map_smul, mul_max] }
le_sup_left := fun _ _ _ => le_max_left _ _
le_sup_right := fun _ _ _ => le_max_right _ _
sup_le := fun _ _ _ h₁ h₂ x => max_le (h₁ x) (h₂ x) }
