inlₗ_mul_inrₗ_eq_toLex — Mathlib

English

In the lexicographic setting, the product of inlₗ m and inrₗ n equals the lexicographic image of (m,n): inlₗ(m) · inrₗ(n) = toLex(m,n).

Русский

В лексикографическом порядке произведение inlₗ m и inrₗ n равно лексикографическому изображению пары (m,n).

LaTeX

$$$$ inl_{\ell}(m) \cdot inr_{\ell}(n) = toLex(m,n). $$$$

Lean4

@[to_additive]
theorem inlₗ_mul_inrₗ_eq_toLex (m : α) (n : β) : inlₗ α β m * inrₗ α β n = toLex (m, n) := by simp [← toLex_mul]

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