English
For a subset R ⊆ M.E, a element e is a coloop in M|R precisely when e is in R and not in the closure of R\{e}.
Русский
Для подмножества R ⊆ M.E элемент e является Coloop в M|R тогда и только тогда, когда e ∈ R и e не лежит в замыкании R\{e}.
LaTeX
$$$\forall {R : Set\,\alpha}, R \subseteq M.E \Rightarrow (M|R).IsColoop e \iff e \notin \overline{R \setminus \{e\}} \land e \in R$$$
Lean4
theorem restrict_isColoop_iff {R : Set α} (hRE : R ⊆ M.E) : (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ { e }) ∧ e ∈ R :=
by
wlog heR : e ∈ R
· exact iff_of_false (fun h ↦ heR h.mem_ground) fun h ↦ heR h.2
rw [isColoop_iff_forall_notMem_isCircuit heR, mem_closure_iff_exists_isCircuit (by simp)]
simp only [restrict_isCircuit_iff hRE, insert_diff_singleton]
aesop
