contract_dep_of_not_subset — Mathlib

English

If K is a circuit and K is not contained in C, then in M / C the set K \ C becomes dependent: (M / C).Dep (K \ C).

Русский

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

LaTeX

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

Lean4

theorem contract_dep_of_not_subset (hK : M.IsCircuit K) {C : Set α} (hKC : ¬K ⊆ C) : (M ／ C).Dep (K \ C) :=
  by
  have h' := hK.contract_isCircuit (C := C ∩ K) (inter_subset_right.ssubset_of_ne (by simpa))
  simp only [diff_inter_self_eq_diff] at h'
  have hwin := h'.contract_dep (C := C \ K) disjoint_sdiff_sdiff
  rwa [contract_contract, inter_union_diff] at hwin

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