delete_diff_isCocircuit — Mathlib

English

If M is a cocircuit, X ⊆ K and X is nonempty, then (M.delete (K \ X)).IsCocircuit X.

Русский

Если M — кокцикл, X ⊆ K и X непусто, то (M.delete(K \ X)).IsCocircuit X.

LaTeX

$$(M.delete (K \ X)).IsCocircuit X$$

Lean4

theorem delete_diff_isCocircuit {X : Set α} (hK : M.IsCocircuit K) (hXK : X ⊆ K) (hX : X.Nonempty) :
    (M ＼ (K \ X)).IsCocircuit X := by
  rw [isCocircuit_def, dual_delete]
  exact hK.isCircuit.contract_diff_isCircuit hX hXK

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