isBasis_iff_indep_subset_closure — Mathlib

English

A set I is a basis of X iff I is independent, I ⊆ X, and X ⊆ cl(I).

Русский

Множество I является базисом X тогда и только тогда, когда I независим, I ⊆ X и X ⊆ cl(I).

LaTeX

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

Lean4

theorem isBasis_iff_indep_subset_closure : M.IsBasis I X ↔ M.Indep I ∧ I ⊆ X ∧ X ⊆ M.closure I :=
  ⟨fun h ↦ ⟨h.indep, h.subset, h.subset_closure⟩, fun h ↦ h.1.isBasis_of_subset_of_subset_closure h.2.1 h.2.2⟩

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