isNonloopAt_iff_inc_not_isLoopAt — Mathlib

English

For all G, e, x, we have IsNonloopAt e x if and only if Inc e x and not IsLoopAt e x.

Русский

Для всех G, e, x верно: IsNonloopAt e x эквивалентно Inc e x и не IsLoopAt e x.

LaTeX

$$$G.IsNonloopAt\\ e\\ x\\;\\Leftrightarrow\\; G.Inc e x \\land \\neg G.IsLoopAt e x$$$

Lean4

theorem isNonloopAt_iff_inc_not_isLoopAt : G.IsNonloopAt e x ↔ G.Inc e x ∧ ¬G.IsLoopAt e x :=
  ⟨fun h ↦ ⟨h.inc, h.not_isLoopAt _⟩, fun ⟨⟨y, hy⟩, hn⟩ ↦ ⟨y, mt (fun h ↦ h ▸ hy) hn, hy⟩⟩

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