semilatticeInf

Mathlib.Order.Preorder.Finsupp

URI: https://scilib.ai/kg/mathlib#Finsupp.semilatticeInf

Lean4

instance semilatticeInf : SemilatticeInf (ι →₀ M)
    where
  inf := zipWith (· ⊓ ·) (inf_idem _)
  inf_le_left _f _g _i := inf_le_left
  inf_le_right _f _g _i := inf_le_right
  le_inf _f _g _i h1 h2 s := le_inf (h1 s) (h2 s)

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

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

Разделы

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

Аффилиация

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