delete_isBasis'_iff — Mathlib

English

(M \\ D).IsBasis' I X iff M.IsBasis' I (X \\ D).

Русский

(M \\ D).IsBasis' I X эквивалентно M.IsBasis' I (X \\ D).

LaTeX

$$(M\\setminus D).IsBasis' I X \\iff M.IsBasis' I (X \\ D)$$

Lean4

@[simp]
theorem delete_isBasis'_iff : (M ＼ D).IsBasis' I X ↔ M.IsBasis' I (X \ D) :=
  by
  rw [isBasis'_iff_isBasis_inter_ground, delete_isBasis_iff, delete_ground, diff_eq, inter_comm M.E, ← inter_assoc, ←
    diff_eq, ← isBasis'_iff_isBasis_inter_ground, and_iff_left_iff_imp, inter_comm, ← inter_diff_assoc]
  exact fun _ ↦ disjoint_sdiff_left

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