instNontrivial — Mathlib

English

If V is nontrivial, there exist two distinct simple graphs on V.

Русский

Если V непустой, существует как минимум два различных простых графа на V.

LaTeX

$$$ \exists G,H : SimpleGraph V, G \neq H $$$

Lean4

instance [Nontrivial V] : Nontrivial (SimpleGraph V) :=
  ⟨⟨⊥, ⊤, fun h ↦
      not_subsingleton V
        ⟨by simpa only [← adj_inj, funext_iff, bot_adj, top_adj, ne_eq, eq_iff_iff, false_iff, not_not] using h⟩⟩⟩

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