simpleGraphOfStructure

Mathlib.ModelTheory.Graph

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.simpleGraphOfStructure

Lean4

/-- Any model of the theory of simple graphs represents a simple graph. -/
@[simps]
def simpleGraphOfStructure [Language.graph.Structure V] [V ⊨ Theory.simpleGraph] : SimpleGraph V
    where
  Adj x y := RelMap adj ![x, y]
  symm :=
    Relations.realize_symmetric.1
      (Theory.realize_sentence_of_mem Theory.simpleGraph (Set.mem_insert_of_mem _ (Set.mem_singleton _)))
  loopless := Relations.realize_irreflexive.1 (Theory.realize_sentence_of_mem Theory.simpleGraph (Set.mem_insert _ _))

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

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

Разделы

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

Аффилиация

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