transfer — Mathlib

English

If I and J are bases on X, X ⊆ Y, and J is a basis on Y, then I is a basis on Y.

Русский

Если I и J — базы на X, X ⊆ Y, и J является базой на Y, то I — база на Y.

LaTeX

$$(M.IsBasis I X) ∧ (M.IsBasis J X) ∧ (X ⊆ Y) ∧ (M.IsBasis J Y) ⇒ M.IsBasis I Y$$

Lean4

theorem transfer (hIX : M.IsBasis I X) (hJX : M.IsBasis J X) (hXY : X ⊆ Y) (hJY : M.IsBasis J Y) : M.IsBasis I Y :=
  by
  rw [← isBase_restrict_iff]; rw [← isBase_restrict_iff] at hJY
  exact hJY.isBase_of_isBasis_superset hJX.subset (hIX.isBasis_restrict_of_subset hXY)

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