English
A cocircuit is a minimal set that intersects every base.
Русский
Кококрит — минимальное множество, пересекающее каждый базис.
LaTeX
$$$M.IsCocircuit(K) \iff Minimal(\lambda X, \forall B, M.IsBase(B) \rightarrow (X \cap B).Nonempty)\ K$$$
Lean4
/-- A cocircuit is a minimal set that intersects every base. -/
theorem isCocircuit_iff_minimal : M.IsCocircuit K ↔ Minimal (fun X ↦ ∀ B, M.IsBase B → (X ∩ B).Nonempty) K :=
by
have aux : M✶.Dep = fun X ↦ (∀ B, M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E := by ext; apply dual_dep_iff_forall
rw [isCocircuit_def, isCircuit_def, aux, iff_comm]
refine
minimal_iff_minimal_of_imp_of_forall (fun _ h ↦ h.1) fun X hX ↦
⟨X ∩ M.E, inter_subset_left, fun B hB ↦ ?_, inter_subset_right⟩
rw [inter_assoc, inter_eq_self_of_subset_right hB.subset_ground]
exact hX B hB
