supsSupHom

Mathlib.Order.Hom.CompleteLattice

URI: https://scilib.ai/kg/mathlib#supsSupHom

← MathLib Explorer

English

The map (a, b) ↦ a ⊔ b is a sSupHom from α × α to α.

Русский

Отображение (a, b) ↦ a ⊔ b является sSupHom из α×α в α.

LaTeX

$$$$ \mathrm{supsSupHom}(a,b) = a \lor b. $$$$

Lean4

/-- The map `(a, b) ↦ a ⊔ b` as a `sSupHom`. -/
def supsSupHom : sSupHom (α × α) α where
  toFun x := x.1 ⊔ x.2
  map_sSup' s := by simp_rw [Prod.fst_sSup, Prod.snd_sSup, sSup_image, iSup_sup_eq]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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