instSupSet

Mathlib.Order.Concept

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

Lean4

instance : SupSet (Concept α β r) :=
  ⟨fun S =>
    { extent := lowerPolar r (⋂ c ∈ S, intent c)
      intent := ⋂ c ∈ S, intent c
      upperPolar_extent := by simp_rw [← upperPolar_extent, ← upperPolar_iUnion₂, upperPolar_lowerPolar_upperPolar]
      lowerPolar_intent := rfl }⟩

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

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

Разделы

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

Аффилиация

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