contract_isCircuit — Mathlib

English

If K is a circuit of M and C is a proper subset of K, then contracting by C yields a circuit in K \ C: (M / C).IsCircuit(K \ C).

Русский

Если K — цикл матроида M, и C ⊂ K, то сжатие по C образует цикл в K \ C: (M / C).IsCircuit(K \ C).

LaTeX

$$(M / C).IsCircuit(K \ C)$$

Lean4

theorem contract_isCircuit (hK : M.IsCircuit K) (hC : C ⊂ K) : (M ／ C).IsCircuit (K \ C) :=
  by
  suffices ∀ e ∈ K, e ∉ C → M.Indep (K \ { e } ∪ C) by
    simpa [isCircuit_iff_dep_forall_diff_singleton_indep, diff_diff_comm (s := K) (t := C), dep_iff,
      (hK.ssubset_indep hC).contract_indep_iff, diff_subset_diff_left hK.subset_ground, disjoint_sdiff_left,
      diff_union_of_subset hC.subset, hK.not_indep]
  exact fun e heK heC ↦ (hK.diff_singleton_indep heK).subset <| by simp [subset_diff_singleton hC.subset heC]

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