isBasis_of_subset_of_subset_closure

English

If I is independent, I ⊆ X, and X ⊆ cl(I), then I is a basis of X.

Русский

Если I независим, I ⊆ X и X ⊆ cl(I), то I является базисом X.

LaTeX

$$$\operatorname{Indep}(I) \land I \subseteq X \land X \subseteq \operatorname{cl}(I) \Rightarrow \mathrm{IsBasis}(I,X)$$$

Lean4

theorem isBasis_of_subset_of_subset_closure (hI : M.Indep I) (hIX : I ⊆ X) (hXI : X ⊆ M.closure I) : M.IsBasis I X :=
  hI.isBasis_closure.isBasis_subset hIX hXI

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