isLoop_iff_closure_eq_loops_and_mem_ground

English

M.IsLoop e is equivalent to closure {e} equals loops and e ∈ E.

Русский

Петля e эквивалентна тому, что closure {e} = loops и e ∈ E.

LaTeX

$$$ M.IsLoop e \iff (M.closure\{e\} = M.loops) \land e \in M.E $$$

Lean4

theorem isLoop_iff_closure_eq_loops_and_mem_ground : M.IsLoop e ↔ M.closure { e } = M.loops ∧ e ∈ M.E
    where
  mp h := ⟨h.closure, h.mem_ground⟩
  mpr
    h := by
    rw [isLoop_iff, ← closure_empty, ← singleton_subset_iff, ← closure_subset_closure_iff_subset_closure, h.1, loops]

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