English
A variant: cocircuit equivalently minimal with condition X ⊆ E.
Русский
Вариант: кококрит эквивалентен минимальности при условии X ⊆ E.
LaTeX
$$$M.IsCocircuit(K) \iff Minimal( \lambda X, ( \neg M.Spanning(M.E \setminus X) \land X \subseteq M.E) ) K$$
Lean4
/-- For an element `e` of a base `B`, the complement of the closure of `B \ {e}` is a cocircuit. -/
theorem compl_closure_diff_singleton_isCocircuit (hB : M.IsBase B) (he : e ∈ B) :
M.IsCocircuit (M.E \ M.closure (B \ { e })) :=
by
rw [isCocircuit_iff_minimal_compl_nonspanning, minimal_subset_iff, diff_diff_cancel_left (M.closure_subset_ground _),
closure_spanning_iff (diff_subset.trans hB.subset_ground)]
have hB' := (isBase_iff_minimal_spanning.1 hB)
refine ⟨fun hsp ↦ hB'.notMem_of_prop_diff_singleton hsp he, fun X hX hXss ↦ hXss.antisymm' ?_⟩
rw [diff_subset_comm]
refine fun f hf ↦ by_contra fun fcl ↦ hX ?_
rw [subset_diff] at hXss
suffices hsp : M.IsBase (insert f (B \ { e }))
by
refine
hsp.spanning.superset <| insert_subset hf <| (M.subset_closure _ (diff_subset.trans hB.subset_ground)).trans ?_
rw [subset_diff, and_iff_left hXss.2.symm]
apply closure_subset_ground
exact hB.exchange_base_of_notMem_closure he fcl
