inl_inf — Mathlib

English

There is a compatibility result for infimum in the left injection: inlₗ(SemilatticeInf.toMin.min a1 a2) = min(inlₗ a1, inlₗ a2), mirroring the infimum in the left component.

Русский

Согласование инфимина через левое вложение: inlₗ(min(a1, a2)) = min(inlₗ a1, inlₗ a2).

LaTeX

$$$ \\mathrm{inl}_{\\ell}(\\mathrm{toMin.min}\\, a_1\\, a_2) = \\mathrm{toMin.min}(\\mathrm{inl}_{\\ell}a_1)(\\mathrm{inl}_{\\ell}a_2) $$$

Lean4

@[simp]
theorem inl_inf (a₁ a₂ : α) : (inlₗ (a₁ ⊓ a₂) : α ⊕ β) = inlₗ a₁ ⊓ inlₗ a₂ :=
  rfl

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