infsInfHom

Mathlib.Order.Hom.CompleteLattice

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

← MathLib Explorer

English

The map (a, b) ↦ a ⊓ b is an sInfHom.

Русский

Отображение (a, b) ↦ a ⊓ b является sInfHom.

LaTeX

$$$$ \mathrm{infsInfHom}(a,b) = a \land b. $$$$

Lean4

/-- The map `(a, b) ↦ a ⊓ b` as an `sInfHom`. -/
def infsInfHom : sInfHom (α × α) α where
  toFun x := x.1 ⊓ x.2
  map_sInf' s := by simp_rw [Prod.fst_sInf, Prod.snd_sInf, sInf_image, iInf_inf_eq]

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

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

Разделы

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

Аффилиация

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