supSet

Mathlib.Combinatorics.SimpleGraph.Basic

URI: https://scilib.ai/kg/mathlib#SimpleGraph.supSet

Lean4

instance supSet : SupSet (SimpleGraph V) where
  sSup
    s :=
    { Adj := fun a b => ∃ G ∈ s, Adj G a b
      symm := fun _ _ => Exists.imp fun _ => And.imp_right Adj.symm
      loopless := by
        rintro a ⟨G, _, ha⟩
        exact ha.ne rfl }

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

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

Разделы

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

Аффилиация

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