delete_spanning_iff — Mathlib

English

If D is coindependent, then (M \ D).Spanning S is equivalent to M.Spanning S and Disjoint S D.

Русский

Если D коиндепендентно, то (M \ D).Spanning S эквивалентно M.Spanning S и Disjoint S D.

LaTeX

$$$ (M \setminus D).Spanning(S) \iff M.Spanning(S) \land Disjoint(S,D) $$$

Lean4

theorem delete_spanning_iff {S : Set α} (hD : M.Coindep D) : (M ＼ D).Spanning S ↔ M.Spanning S ∧ Disjoint S D :=
  by
  simp only [spanning_iff_exists_isBase_subset', hD.delete_isBase_iff, and_assoc, delete_ground, subset_diff,
    and_congr_left_iff, and_imp]
  refine fun hSE hSD ↦ ⟨fun ⟨B, hB, hBD, hBS⟩ ↦ ⟨B, hB, hBS⟩, fun ⟨B, hB, hBS⟩ ↦ ⟨B, hB, ?_, hBS⟩⟩
  exact hSD.mono_left hBS

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