English
The left injection preserves the supremum, i.e., inlₗ(a1 ⊔ a2) equals inlₗ a1 ⊔ inlₗ a2, and the right injection preserves the supremum in the right slot, i.e., inrₗ(b1 ⊔ b2) equals inrₗ b1 ⊔ inrₗ b2; similarly for infimum.
Русский
Левое вложение сохраняет верхнюю границу, то есть inlₗ(a1 ⊔ a2) = inlₗ a1 ⊔ inlₗ a2, и правое вложение сохраняет верхнюю границу в правой части, т.е. inrₗ(b1 ⊔ b2) = inrₗ b1 ⊔ inrₗ b2; аналогично для Inf.
LaTeX
$$$\\text{inl}_{\\ell}(a_1 \\sqcup a_2) = \\text{inl}_{\\ell} a_1 \\sqcup \\text{inl}_{\\ell} a_2$, \\\\ $\\text{inr}_{\\ell}(b_1 \\sqcup b_2) = \\text{inr}_{\\ell} b_1 \\sqcup \\text{inr}_{\\ell} b_2$$$
Lean4
@[simp]
theorem inl_sup (a₁ a₂ : α) : (inlₗ (a₁ ⊔ a₂) : α ⊕ β) = inlₗ a₁ ⊔ inlₗ a₂ :=
rfl
