inr_sup — Mathlib

English

The right injection preserves the infimum, i.e., inrₗ(b1 ⊓ b2) = inrₗ b1 ⊓ inrₗ b2, and similarly for supremum

Русский

Правое вложение сохраняет наименьшее, то есть inrₗ(b1 ⊓ b2) = inrₗ b1 ⊓ inrₗ b2; аналогично для supremum

LaTeX

$$$ \\mathrm{inr}_{\\ell}(b_1 \\sqcap b_2) = \\mathrm{inr}_{\\ell} b_1 \\sqcap \\mathrm{inr}_{\\ell} b_2$$$

Lean4

@[simp]
theorem inr_sup (b₁ b₂ : β) : (inrₗ (b₁ ⊔ b₂) : α ⊕ β) = inrₗ b₁ ⊔ inrₗ b₂ :=
  rfl

Похожие утверждения