inter_isBasis_closure_iff_subset_closure_inter

English

For I independent, X a subset, M.IsBasis(X ∩ I, X) if and only if X ⊆ closure(X ∩ I).

Русский

Для I независимого: M.IsBasis(X ∩ I, X) эквивалентно X ⊆ closure(X ∩ I).

LaTeX

$$$M.IsBasis (X \cap I) X \iff X \subseteq M.closure (X \cap I)$$$

Lean4

theorem inter_isBasis_closure_iff_subset_closure_inter {X : Set α} (hI : M.Indep I) :
    M.IsBasis (X ∩ I) X ↔ X ⊆ M.closure (X ∩ I) :=
  ⟨IsBasis.subset_closure, (hI.inter_left X).isBasis_of_subset_of_subset_closure inter_subset_left⟩

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