English
For every independent set I of M and element e ∈ I, there exists a cocircuit K such that K ∩ I = {e}.
Русский
Для каждого независимого множества I матроида M и элемента e ∈ I существует кококарта K такая, что K ∩ I = {e}.
LaTeX
$$$\exists K, M.IsCocircuit K \land K \cap I = \{ e \}$$$
Lean4
/-- For every element `e` of an independent set `I`,
there is a cocircuit whose intersection with `I` is `{e}`. -/
theorem exists_isCocircuit_inter_eq_mem (hI : M.Indep I) (heI : e ∈ I) : ∃ K, M.IsCocircuit K ∧ K ∩ I = { e } :=
by
obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset
refine ⟨M.fundCocircuit e B, fundCocircuit_isCocircuit (hIB heI) hB, ?_⟩
rw [subset_antisymm_iff, subset_inter_iff, singleton_subset_iff, and_iff_right (mem_fundCocircuit _ _ _),
singleton_subset_iff, and_iff_left heI, ← M.fundCocircuit_inter_eq (hIB heI)]
exact inter_subset_inter_right _ hIB
