isBasis'_restrict_iff — Mathlib

English

For any R, I, X: (M|R).IsBasis' I X iff M.IsBasis' I (X ∩ R) and I ⊆ R.

Русский

Для любых R, I, X: (M|R).IsBasis' I X эквивалентно M.IsBasis' I (X ∩ R) и I ⊆ R.

LaTeX

$$$ (M \\restriction R).IsBasis' I X \\iff (M.IsBasis' I (X \\cap R) \\land I \\subseteq R) $$$

Lean4

theorem isBasis'_restrict_iff : (M ↾ R).IsBasis' I X ↔ M.IsBasis' I (X ∩ R) ∧ I ⊆ R :=
  by
  simp_rw [IsBasis', maximal_iff, restrict_indep_iff, subset_inter_iff, and_imp]
  tauto

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