instMin

Mathlib.Order.Nucleus

URI: https://scilib.ai/kg/mathlib#Nucleus.instMin

Lean4

instance : Min (Nucleus X) where
  min m
    n :=
    { toFun := m ⊓ n
      map_inf' x y := by simp [inf_inf_inf_comm]
      idempotent'
        x := by
        simp only [Pi.inf_apply, map_inf, idempotent]
        exact inf_le_inf inf_le_left inf_le_right
      le_apply' x := le_inf m.le_apply n.le_apply }

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

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

Разделы

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

Аффилиация

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