English
ValuationSubring K has a SemilatticeSup structure with join defined by a canonical construction from R and S.
Русский
У ValuationSubring K существует структура SemilatticeSup, где верхний предел задаётся каноническим образом через R и S.
LaTeX
$$$\text{instSemilatticeSup}(K)$ with $R\lor S := \mathrm{ofLE}(R, R\lor S, le\_sup\_left)$$$
Lean4
instance : SemilatticeSup (ValuationSubring K) :=
{
(inferInstance :
PartialOrder
(ValuationSubring
K)) with
sup := fun R S => ofLE R (R.toSubring ⊔ S.toSubring) <| le_sup_left
le_sup_left := fun R S _ hx => (le_sup_left : R.toSubring ≤ R.toSubring ⊔ S.toSubring) hx
le_sup_right := fun R S _ hx => (le_sup_right : S.toSubring ≤ R.toSubring ⊔ S.toSubring) hx
sup_le := fun R S T hR hT _ hx => (sup_le hR hT : R.toSubring ⊔ S.toSubring ≤ T.toSubring) hx }
