simpleGraph_model — Mathlib

English

If G is a SimpleGraph on V, then G defines a model of Theory.simpleGraph.

Русский

Если G является простым графом на множестве V, то G задаёт модель Theory.simpleGraph.

LaTeX

$$$G:\text{SimpleGraph } V \rightarrow \text{Theory.Model } V\, Theory.simpleGraph$$$

Lean4

instance simpleGraph_model (G : SimpleGraph V) : @Theory.Model _ V G.structure Theory.simpleGraph :=
  by
  letI := G.structure
  rw [Theory.simpleGraph_model_iff]
  exact ⟨G.loopless, G.symm⟩

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