isCocircuit_iff_minimal_compl_nonspanning'

English

A version with explicit support: cocircuit iff minimal with properties on X ⊆ E.

Русский

Версия с поддержкой: кококрит эквивалентна минимальности, когда X ⊆ E.

LaTeX

$$$M.IsCocircuit(K) \iff Minimal(\lambda X, \mathrm{Not}(M.Spanning(M.E \setminus X)) \land X \subseteq M.E) K$$

Lean4

/-- A version of `Matroid.isCocircuit_iff_minimal_compl_nonspanning` with a support assumption
in the minimality. -/
theorem isCocircuit_iff_minimal_compl_nonspanning' :
    M.IsCocircuit K ↔ Minimal (fun X ↦ ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K :=
  by
  rw [isCocircuit_iff_minimal_compl_nonspanning]
  exact
    minimal_iff_minimal_of_imp_of_forall (fun _ h ↦ h.1)
      (fun X hX ↦ ⟨X ∩ M.E, inter_subset_left, by rwa [diff_inter_self_eq_diff], inter_subset_right⟩)

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