sup_apply

Mathlib.Data.DFinsupp.Order

URI: https://scilib.ai/kg/mathlib#DFinsupp.sup_apply

English

For f,g in DFinsupp and i in ι, the i-th coordinate of f ⊔ g equals f(i) ⊔ g(i).

Русский

Для f,g в DFinsupp и некоторого i из ι, i-я координата (f ⊔ g) равна f(i) ⊔ g(i).

LaTeX

$$$$ (f \sup g)(i) = f(i) \sup g(i) \quad \text{for all } i. $$$$

Lean4

theorem sup_apply [∀ i, SemilatticeSup (α i)] (f g : Π₀ i, α i) (i : ι) : (f ⊔ g) i = f i ⊔ g i :=
  zipWith_apply _ _ _ _ _

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

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

Разделы

Аффилиация

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