isBasis_isRestriction — Mathlib

English

If I is a basis for M on X and N ≤r M with X ⊆ N.E, then N is a basis for M on X.

Русский

Если I — база M на X и N ≤r M и X ⊆ N.E, то N является базой M на X.

LaTeX

$$$ (M.IsBasis I X) \land (N \le_r M) \land (X \subseteq N.E) \Rightarrow N.IsBasis I X $$$

Lean4

theorem isBasis_isRestriction (hI : M.IsBasis I X) (hNM : N ≤r M) (hX : X ⊆ N.E) : N.IsBasis I X := by
  obtain ⟨R, hR, rfl⟩ := hNM; rwa [isBasis_restrict_iff, and_iff_left (show X ⊆ R from hX)]

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