simpleGraph_model_iff — Mathlib

English

A model satisfies Theory.simpleGraph iff the adjacency relation is irreflexive and symmetric.

Русский

Модель удовлетворяет Theory.simpleGraph тогда, когда отношение смежности иррефлексивно и симметрично.

LaTeX

$$$V \models Theory.simpleGraph \iff (\operatorname{Irreflexive}(\lambda x,y: RelMap adj ![x,y])) \land (\operatorname{Symmetric}(\lambda x,y: RelMap adj ![x,y]))$$$

Lean4

@[simp]
theorem simpleGraph_model_iff [Language.graph.Structure V] :
    V ⊨ Theory.simpleGraph ↔
      (Irreflexive fun x y : V => RelMap adj ![x, y]) ∧ Symmetric fun x y : V => RelMap adj ![x, y] :=
  by simp [Theory.simpleGraph]

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