subset — Mathlib

English

If X has IsRkFinite and Y ⊆ X, then Y also has IsRkFinite.

Русский

Если X имеет IsRkFinite и Y ⊆ X, то Y тоже имеет IsRkFinite.

LaTeX

$$$ \\text{If } h : M.IsRkFinite X \\text{ and } Y \\subseteq X, \\text{ then } M.IsRkFinite Y $$$

Lean4

theorem subset (h : M.IsRkFinite X) (hXY : Y ⊆ X) : M.IsRkFinite Y :=
  by
  obtain ⟨I, hI⟩ := M.exists_isBasis' Y
  obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis'_of_subset (hI.subset.trans hXY)
  exact hI.isRkFinite_of_finite <| (hJ.finite_of_isRkFinite h).subset hIJ

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