sup_mul — Mathlib

English

The product distributes over supremum on the right: M * (N ⊔ P) = M * N ⊔ M * P.

Русский

Произведение распределяется по верхнему объединению справа: M * (N ⊔ P) = M * N ⊔ M * P.

LaTeX

$$$ M * (N \sqcup P) = M * N \sqcup M * P $$$

Lean4

theorem sup_mul : (M ⊔ N) * P = M * P ⊔ N * P :=
  le_antisymm
    (mul_le.mpr fun mn hmn p hp ↦ by
      obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn
      rw [right_distrib]; exact add_mem_sup (mul_mem_mul hm hp) <| mul_mem_mul hn hp)
    (sup_le (mul_le_mul_left le_sup_left) <| mul_le_mul_left le_sup_right)

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