isBasis'_iff_isBasis_inter_ground

English

A Basis' I X is equivalent to I being a basis of X ∩ E.

Русский

База' I X эквивалентна тому, что I — база X ∩ E.

LaTeX

$$$ M.IsBasis' I X \iff M.IsBasis I (X \cap M.E) $$$

Lean4

theorem isBasis'_iff_isBasis_inter_ground : M.IsBasis' I X ↔ M.IsBasis I (X ∩ M.E) :=
  by
  rw [IsBasis', IsBasis, and_iff_left inter_subset_right, maximal_iff_maximal_of_imp_of_forall]
  · exact fun I hI ↦ ⟨hI.1, hI.2.trans inter_subset_left⟩
  exact fun I hI ↦ ⟨I, rfl.le, hI.1, subset_inter hI.2 hI.1.subset_ground⟩

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