contract_restrict_eq_restrict_contract

English

Contraction and deletion commute for disjoint sets: M / C \ D = M \ D / C.

Русский

Сжатие и удаление коммутируют для непересекающихся множеств: M / C \ D = M \ D / C.

LaTeX

$$M / C \ D = M \ D / C$$

Lean4

theorem contract_restrict_eq_restrict_contract (M : Matroid α) (h : Disjoint C R) : (M ／ C) ↾ R = (M ↾ (R ∪ C)) ／ C :=
  by
  refine ext_indep (by simp [h.sdiff_eq_right]) fun I (hI : I ⊆ R) ↦ ?_
  obtain ⟨J, hJ⟩ := (M ↾ (R ∪ C)).exists_isBasis' C
  have hJ' : M.IsBasis' J C := by
    simpa [inter_eq_self_of_subset_left subset_union_right] using (isBasis'_restrict_iff.1 hJ).1
  rw [restrict_indep_iff, hJ.contract_indep_iff, hJ'.contract_indep_iff, restrict_indep_iff]
  have hJC := hJ'.subset
  tauto_set

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