English
Let B be a base with e ∈ B. Then M.IsColoop e is equivalent to: for all x ∈ E \\ B, e ∉ fundCircuit x B.
Русский
Пусть B — базис с e ∈ B. Тогда M.IsColoop e эквивалентно: для всех x ∈ E \\ B, e ∉ fundCircuit x B.
LaTeX
$$$\\forall B\\, (M.IsBase B \\to (e \\in B)) \\Rightarrow (M.IsColoop e \\iff \\forall x\\in M.E \\setminus B, e \\notin M.fundCircuit x B)$$$
Lean4
theorem isColoop_iff_forall_notMem_fundCircuit (hB : M.IsBase B) (he : e ∈ B) :
M.IsColoop e ↔ ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B :=
by
refine ⟨fun h x hx heC ↦ (h.notMem_isCircuit <| hB.fundCircuit_isCircuit hx.1 hx.2) heC, fun h ↦ ?_⟩
have h' : M.E \ { e } ⊆ M.closure (B \ { e }) :=
by
rintro x ⟨hxE, hne : x ≠ e⟩
obtain (hx | hx) := em (x ∈ B)
· exact M.subset_closure (B \ { e }) (diff_subset.trans hB.subset_ground) ⟨hx, hne⟩
have h_cct := (hB.fundCircuit_isCircuit hxE hx).mem_closure_diff_singleton_of_mem (M.mem_fundCircuit x B)
refine (M.closure_subset_closure (subset_diff_singleton ?_ ?_)) h_cct
· simpa using fundCircuit_subset_insert ..
simp [hne.symm, h x ⟨hxE, hx⟩]
rw [isColoop_iff_notMem_closure_compl (hB.subset_ground he)]
exact notMem_subset (M.closure_subset_closure_of_subset_closure h') <| hB.indep.notMem_closure_diff_of_mem he
