map_sup

Mathlib.Order.RelIso.Set

URI: https://scilib.ai/kg/mathlib#RelHomClass.map_sup

← MathLib Explorer

English

A RelHom preserves supremum: a(m ⊔ n) = a m ⊔ a n.

Русский

Гомоморфизм RelHom сохраняет наибольший: a(m ⊔ n) = a m ⊔ a n.

LaTeX

$$$$ a(m \vee n) = a m \vee a n. $$$$

Lean4

theorem map_sup [SemilatticeSup α] [LinearOrder β] [FunLike F β α] [RelHomClass F (· > ·) (· > ·)] (a : F) (m n : β) :
    a (m ⊔ n) = a m ⊔ a n :=
  map_inf (α := αᵒᵈ) (β := βᵒᵈ) _ _ _

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

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

Разделы

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

Аффилиация

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