isCocircuit_iff_minimal_compl_nonspanning

English

A cocircuit is minimal with respect to the property that its complement does not span the ground set.

Русский

Кококрит минимален по свойству того, что его дополнение не порождает всё основание.

LaTeX

$$$M.IsCocircuit(K) \iff Minimal(\lambda X, \neg M.Spanning(M.E \setminus X)) K$$

Lean4

/-- A cocircuit is a minimal set whose complement is nonspanning. -/
theorem isCocircuit_iff_minimal_compl_nonspanning : M.IsCocircuit K ↔ Minimal (fun X ↦ ¬M.Spanning (M.E \ X)) K :=
  by
  convert isCocircuit_iff_minimal with K
  simp_rw [spanning_iff_exists_isBase_subset (S := M.E \ K), not_exists, subset_diff, not_and,
    not_disjoint_iff_nonempty_inter, ← and_imp, and_iff_left_of_imp IsBase.subset_ground, inter_comm K]

Похожие утверждения