contract_dep — Mathlib

English

If K is a circuit of M and C is disjoint from K, then in the contracted matroid M / C, the set K remains dependent: (M / C).Dep K.

Русский

Если K — цикл матроида M и C не пересекает K, то в сжатом матроиде M / C множество K остается зависимым: (M / C).Dep K.

LaTeX

$$(M / C).Dep K$$

Lean4

theorem contract_dep (hK : M.IsCircuit K) (hCK : Disjoint C K) : (M ／ C).Dep K :=
  by
  obtain ⟨I, hI⟩ := M.exists_isBasis (C ∩ M.E)
  rw [← contract_inter_ground_eq, Dep, hI.contract_indep_iff, and_iff_left (hCK.mono_left inter_subset_left),
    contract_ground, subset_diff, and_iff_left (hCK.symm.mono_right inter_subset_left), and_iff_left hK.subset_ground]
  exact fun hi ↦ hK.dep.not_indep (hi.subset subset_union_left)

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