isBasis_of_isBasis_of_subset_of_subset

English

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

Русский

Если I — база на X и J — база на Y, причём J ⊆ X и I ⊆ Y, то I — база на Y.

LaTeX

$$M.IsBasis I X → M.IsBasis J Y → J ⊆ X → I ⊆ Y → M.IsBasis I Y$$

Lean4

theorem isBasis_of_isBasis_of_subset_of_subset (hI : M.IsBasis I X) (hJ : M.IsBasis J Y) (hJX : J ⊆ X) (hIY : I ⊆ Y) :
    M.IsBasis I Y := by
  have hI' := hI.isBasis_subset (subset_inter hI.subset hIY) inter_subset_left
  have hJ' := hJ.isBasis_subset (subset_inter hJX hJ.subset) inter_subset_right
  exact hI'.transfer hJ' inter_subset_right hJ

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