union_indep_iff_contract_indep — Mathlib

English

If I is independent in M, then M.Indep(I ∪ J) holds if and only if (M / I).Indep(J \ I).

Русский

Если I независимо в M, то M независим по I ∪ J тогда и только тогда, когда (M / I).Indep(J \ I).

LaTeX

$$$ M.Indep(I \cup J) \iff (M / I).Indep(J \ I) $$$

Lean4

theorem union_indep_iff_contract_indep (hI : M.Indep I) : M.Indep (I ∪ J) ↔ (M ／ I).Indep (J \ I) := by
  rw [hI.contract_indep_iff, and_iff_right disjoint_sdiff_left, diff_union_self, union_comm]

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