delete_isBasis_iff — Mathlib

English

For any I, X, (M \\ D).IsBasis I X iff M.IsBasis I X ∧ Disjoint X D.

Русский

Для любых I, X: (M \\ D).IsBasis I X эквивалентно M.IsBasis I X и Disjoint X D.

LaTeX

$$$(M\\setminus D).IsBasis I X \\iff (M.IsBasis I X) \\land Disjoint(X,D)$$$

Lean4

@[simp]
theorem delete_isBasis_iff : (M ＼ D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D := by
  rw [← restrict_compl, isBasis_restrict_iff, subset_diff, ← and_assoc, and_iff_left_of_imp IsBasis.subset_ground]

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