diff_indep_iff_indep_of_subset_coloops

English

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

Русский

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

LaTeX

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

Lean4

theorem diff_indep_iff_indep_of_subset_coloops (hK : K ⊆ M.coloops) : M.Indep (I \ K) ↔ M.Indep I := by
  rw [← union_indep_iff_indep_of_subset_coloops hK, diff_union_self, union_indep_iff_indep_of_subset_coloops hK]

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