instSupConcept

Mathlib.Order.Concept

URI: https://scilib.ai/kg/mathlib#Concept.instSupConcept

Lean4

instance instSupConcept : Max (Concept α β r) :=
  ⟨fun c d =>
    { extent := lowerPolar r (c.intent ∩ d.intent)
      intent := c.intent ∩ d.intent
      upperPolar_extent := by
        rw [← c.upperPolar_extent, ← d.upperPolar_extent, ← upperPolar_union, upperPolar_lowerPolar_upperPolar]
      lowerPolar_intent := rfl }⟩

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

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

Разделы

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

Аффилиация

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