instNontrivialOfNonempty — Mathlib

English

There exist at least two distinct digraphs on V; i.e., the class of digraphs on V is nontrivial whenever V is nonempty.

Русский

Существует хотя бы два различные ориентированных графа на V; класс графов на V не тривиален при непустом V.

LaTeX

$$$\\exists G,H: \\mathrm{Digraph}(V),\\ G \\neq H$$$

Lean4

instance [Nonempty V] : Nontrivial (Digraph V) := by
  use ⊥, ⊤
  have v := Classical.arbitrary V
  exact ne_of_apply_ne (·.Adj v v) (by simp)

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