iSup_mul

Mathlib.Data.ENat.Lattice

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

English

Multiplication on the right distributes over iSup: (⨆ i, f i) * a = ⨆ i, f i * a.

Русский

Умножение справа на фиксированное ENat распределяется над iSup: (⨆ i, f i) * a = ⨆ i, f i * a.

LaTeX

$$$(\sup_i f(i)) * a = \sup_i (f(i) * a)$$$

Lean4

theorem iSup_mul (f : ι → ℕ∞) (a : ℕ∞) : (⨆ i, f i) * a = ⨆ i, f i * a := by simp_rw [mul_comm, ENat.mul_iSup]

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

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

Разделы

Аффилиация

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