not_isNonloop_iff_closure — Mathlib

English

Not a nonloop e is equivalent to closure of {e} equals the loops set.

Русский

Не-не-петля e эквивалентна тому, что замыкание {e} равно петлям.

LaTeX

$$$ \neg M.IsNonloop e \iff M.closure \{ e \} = M.loops $$$

Lean4

theorem not_isNonloop_iff_closure : ¬M.IsNonloop e ↔ M.closure { e } = M.loops :=
  by
  by_cases he : e ∈ M.E
  · simp [isLoop_iff_closure_eq_loops_and_mem_ground, he]
  simp [← closure_inter_ground, singleton_inter_eq_empty.2 he, loops,
    (show ¬M.IsNonloop e from fun h ↦ he h.mem_ground)]

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