contract_indep_iff — Mathlib

English

If I is independent in M, then (M / I) is independent on J if and only if J is disjoint from I and M is independent on J ∪ I.

Русский

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

LaTeX

$$$ (M / I).Indep J \Leftrightarrow (Disjoint J I) \land M.Indep(J \cup I) $$$

Lean4

theorem contract_indep_iff (hI : M.Indep I) : (M ／ I).Indep J ↔ Disjoint J I ∧ M.Indep (J ∪ I) :=
  by
  simp_rw [indep_iff, hI.contract_isBase_iff, union_subset_iff]
  exact
    ⟨fun ⟨B, ⟨hBI, hdj⟩, hJB⟩ ↦
      ⟨disjoint_of_subset_left hJB hdj, _, hBI, hJB.trans subset_union_left, subset_union_right⟩,
      fun ⟨hdj, B, hB, hJB, hIB⟩ ↦
      ⟨B \ I, ⟨by simpa [union_eq_self_of_subset_right hIB], disjoint_sdiff_left⟩, subset_diff.2 ⟨hJB, hdj⟩⟩⟩

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