delete_isCocircuit — Mathlib

English

If K is a cocircuit of M and D ⊂ K, then deleting D preserves the cocircuit: (M \ D).IsCocircuit (K \ D).

Русский

Если K — кокцикл M и D ⊂ K, то удаление D сохраняет кокцикл: (M \ D).IsCocircuit(K \ D).

LaTeX

$$(M \ D).IsCocircuit(K \ D)$$

Lean4

theorem delete_isCocircuit {D : Set α} (hK : M.IsCocircuit K) (hD : D ⊂ K) : (M ＼ D).IsCocircuit (K \ D) :=
  by
  rw [isCocircuit_def, dual_delete]
  exact hK.isCircuit.contract_isCircuit hD

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