isBasis_union_iff_indep_closure — Mathlib

English

A subset I is a basis of I ∪ X if and only if I is independent and X ⊆ closure(I).

Русский

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

LaTeX

$$$M.IsBasis I (I \cup X) \iff M.Indep I \land X \subseteq M.closure I$$$

Lean4

theorem isBasis_union_iff_indep_closure : M.IsBasis I (I ∪ X) ↔ M.Indep I ∧ X ⊆ M.closure I :=
  ⟨fun h ↦ ⟨h.indep, subset_union_right.trans h.subset_closure⟩, fun ⟨hI, hXI⟩ ↦
    hI.isBasis_closure.isBasis_subset subset_union_left (union_subset (M.subset_closure I) hXI)⟩

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