English
In the Lex sum, the left embedding is a lattice homomorphism, i.e., it preserves both supremum and infimum when embedding α into α ⊕ₗ β.
Русский
В лексикографической сумме левое вложение является гомоморфизмом частичного порядка: сохраняет верхнюю и нижнюю границы (супы и инфимы).
LaTeX
$$$ \\text{inl}_{\\ell} \\; \\text{ preserves } \\sqcup \\\\text{and } \\sqcap: \\; \\mathrm{inl}_{\\ell}(a_1 \\sqcup a_2) = \\mathrm{inl}_{\\ell} a_1 \\sqcup \\mathrm{inl}_{\\ell} a_2, \\; \\mathrm{inl}_{\\ell}(a_1 \\sqcap a_2) = \\mathrm{inl}_{\\ell} a_1 \\sqcap \\mathrm{inl}_{\\ell} a_2. $$$
Lean4
instance instSemilatticeSup : SemilatticeSup (α ⊕ₗ β)
where
sup
| inlₗ a₁, inlₗ a₂ => inl (a₁ ⊔ a₂)
| inlₗ a₁, inrₗ b₂ => inr b₂
| inrₗ b₁, inlₗ a₂ => inr b₁
| inrₗ b₁, inrₗ b₂ => inr (b₁ ⊔ b₂)
le_sup_left
| inlₗ a₁, inlₗ a₂ => inl_le_inl_iff.2 le_sup_left
| inlₗ a₁, inrₗ b₂ => inl_le_inr _ _
| inrₗ b₁, inlₗ a₂ => le_rfl
| inrₗ b₁, inrₗ b₂ => inr_le_inr_iff.2 le_sup_left
le_sup_right
| inlₗ a₁, inlₗ a₂ => inl_le_inl_iff.2 le_sup_right
| inlₗ a₁, inrₗ b₂ => le_rfl
| inrₗ b₁, inlₗ a₂ => inl_le_inr _ _
| inrₗ b₁, inrₗ b₂ => inr_le_inr_iff.2 le_sup_right
sup_le
| inlₗ a₁, inlₗ a₂, inlₗ a₃, Lex.inl h₁₃, Lex.inl h₂₃ => inl_le_inl_iff.2 <| sup_le h₁₃ h₂₃
| inlₗ a₁, inlₗ a₂, inrₗ b₃, Lex.sep _ _, Lex.sep _ _ => Lex.sep _ _
| inlₗ a₁, inrₗ b₂, inrₗ b₃, Lex.sep _ _, Lex.inr h₂₃ => inr_le_inr_iff.2 h₂₃
| inrₗ b₁, inlₗ a₂, inrₗ b₃, Lex.inr h₁₃, Lex.sep _ _ => inr_le_inr_iff.2 h₁₃
| inrₗ b₁, inrₗ b₂, inrₗ b₃, Lex.inr h₁₃, Lex.inr h₂₃ => inr_le_inr_iff.2 <| sup_le h₁₃ h₂₃
