isBasis_restrict_iff' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isBasis_restrict_iff' : (M ↾ R).IsBasis I X ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ R :=
  by
  rw [isBasis_iff_isBasis'_subset_ground, isBasis'_restrict_iff, restrict_ground_eq, and_congr_left_iff, ←
    isBasis'_iff_isBasis_inter_ground]
  intro hXR
  rw [inter_eq_self_of_subset_left hXR, and_iff_left_iff_imp]
  exact fun h ↦ h.subset.trans hXR

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