instMax

Mathlib.Order.Hom.Bounded

URI: https://scilib.ai/kg/mathlib#BotHom.instMax

English

If β has a semilattice-sup and an order-bottom, the supremum of BotHoms is defined pointwise: (f ⊔ g)(x) = f(x) ⊔ g(x).

Русский

Если β имеет верхнюю грань и т. п., то супремум BotHom задаётся точечно: (f ⊔ g)(x) = f(x) ⊔ g(x).

LaTeX

$$$(f \\sup g)(x) = f(x) \\sup g(x).$$$

Lean4

instance : Max (BotHom α β) :=
  ⟨fun f g => ⟨f ⊔ g, by rw [Pi.sup_apply, map_bot, map_bot, sup_bot_eq]⟩⟩

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

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

Разделы

Аффилиация

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