isLoopAt_or_isNonloopAt — Mathlib

English

For any edge e and vertex x, either e is a loop at x or e is nonloop at x.

Русский

Для любого ребра e и вершины x либо e является петлей в x, либо e — некольцевое по отношению к x.

LaTeX

$$$\\forall e\\,\\forall x\\, G.IsLoopAt e x \\lor G.IsNonloopAt e x$$$

Lean4

theorem isLoopAt_or_isNonloopAt (h : G.Inc e x) : G.IsLoopAt e x ∨ G.IsNonloopAt e x := by
  simp [isNonloopAt_iff_inc_not_isLoopAt, h, em]

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