mul_sSup

Mathlib.Data.ENat.Lattice

URI: https://scilib.ai/kg/mathlib#ENat.mul_sSup

English

Multiplication distributes over sSup from the left: a * sSup s = ⨆ b ∈ s, a * b.

Русский

Умножение слева на sSup распространяется: a * sSup s = ⨆ b ∈ s, a * b.

LaTeX

$$$a * \mathrm{sSup}(s) = \bigl(\bigsqcup_{b \in s} (a * b)\bigr)$$$

Lean4

theorem mul_sSup : a * sSup s = ⨆ b ∈ s, a * b := by simp_rw [sSup_eq_iSup, mul_iSup]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru