delete_isBase_iff — Mathlib

English

If D is coindependent in M, then (M \ D).IsBase B holds exactly when M.IsBase B and B is disjoint from D.

Русский

Если D сопринжированно не является зависимым в M, то (M \ D).IsBase B эквивалентно M.IsBase B и Disjoint B D.

LaTeX

$$$ (M \setminus D).IsBase B \iff M.IsBase B \land Disjoint B D $$$

Lean4

theorem delete_isBase_iff (hD : M.Coindep D) : (M ＼ D).IsBase B ↔ M.IsBase B ∧ Disjoint B D :=
  by
  rw [Matroid.delete_isBase_iff]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · have hss := h.subset
    rw [subset_diff] at hss
    have hcl := h.isBasis_closure_right
    rw [hD.closure_compl, isBasis_ground_iff] at hcl
    exact ⟨hcl, hss.2⟩
  exact h.1.isBasis_ground.isBasis_subset (by simp [subset_diff, h.1.subset_ground, h.2]) diff_subset

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