union_indep_iff_indep_of_subset_coloops

English

If K ⊆ M.coloops, then I ∪ K is independent in M iff I is independent in M.

Русский

Если K ⊆ M.coloops, то I ∪ K независимо тогда и только тогда, когда I независимо.

LaTeX

$$$$ K \subseteq M.coloops \Rightarrow M.Indep(I \cup K) \iff M.Indep(I). $$$$

Lean4

theorem union_indep_iff_indep_of_subset_coloops (hK : K ⊆ M.coloops) : M.Indep (I ∪ K) ↔ M.Indep I :=
  by
  refine ⟨fun h ↦ h.subset subset_union_left, fun h ↦ ?_⟩
  obtain ⟨B, hB, hIB⟩ := h.exists_isBase_superset
  exact hB.indep.subset (union_subset hIB (hK.trans fun e he ↦ IsColoop.mem_of_isBase he hB))

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