English
Given SemilatticeInf α and SemilatticeInf β, the Lex sum α ⊕ₗ β carries a SemilatticeInf structure extending the componentwise operations as defined, i.e., the infimum is defined by the Lex rules on the sum.
Русский
При наличии полупорядования по Inf в α и β лексикографическая сумма α ⊕ₗ β образует структуру SemilatticeInf, наследуя операции инфимина по правилам Lex.
LaTeX
$$$ \\text{instSemilatticeInf} : \\text{SemilatticeInf}(\\alpha \\oplus_{\\ell} \\beta) $ with inf defined by Lex rules$$
Lean4
instance instSemilatticeInf : SemilatticeInf (α ⊕ₗ β)
where
inf
| inlₗ a₁, inlₗ a₂ => inl (a₁ ⊓ a₂)
| inlₗ a₁, inrₗ b₂ => inl a₁
| inrₗ b₁, inlₗ a₂ => inl a₂
| inrₗ b₁, inrₗ b₂ => inr (b₁ ⊓ b₂)
inf_le_left
| inlₗ a₁, inlₗ a₂ => inl_le_inl_iff.2 inf_le_left
| inlₗ a₁, inrₗ b₂ => le_rfl
| inrₗ b₁, inlₗ a₂ => inl_le_inr _ _
| inrₗ b₁, inrₗ b₂ => inr_le_inr_iff.2 inf_le_left
inf_le_right
| inlₗ a₁, inlₗ a₂ => inl_le_inl_iff.2 inf_le_right
| inlₗ a₁, inrₗ b₂ => inl_le_inr _ _
| inrₗ b₁, inlₗ a₂ => le_rfl
| inrₗ b₁, inrₗ b₂ => inr_le_inr_iff.2 inf_le_right
le_inf
| inlₗ a₁, inlₗ a₂, inlₗ a₃, Lex.inl h₁₃, Lex.inl h₂₃ => inl_le_inl_iff.2 <| le_inf h₁₃ h₂₃
| inlₗ a₁, inlₗ a₂, inrₗ b₃, Lex.inl h₁₃, Lex.sep _ _ => inl_le_inl_iff.2 h₁₃
| inlₗ a₁, inrₗ b₂, inlₗ a₃, Lex.sep _ _, Lex.inl h₂₃ => inl_le_inl_iff.2 h₂₃
| inlₗ a₁, inrₗ b₂, inrₗ b₃, Lex.sep _ _, Lex.sep _ _ => Lex.sep _ _
| inrₗ b₁, inrₗ b₂, inrₗ b₃, Lex.inr h₁₃, Lex.inr h₂₃ => inr_le_inr_iff.2 <| le_inf h₁₃ h₂₃
