contract_indep_iff — Mathlib

English

If I is a basis' for X, then (M ／ X).Indep J iff M.Indep (J ∪ I) ∧ Disjoint X J.

Русский

Если I является базисом' X, то (M ／ X).Indep J эквивалентно M.indep(J ∪ I) и Disjoint(X,J).

LaTeX

$$$ (M ／ X).Indep J \iff M.Indep(J \cup I) \land Disjoint X J $$$

Lean4

theorem contract_indep_iff (hI : M.IsBasis' I X) : (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J := by
  rw [hI.contract_eq_contract_delete, delete_indep_iff, hI.indep.contract_indep_iff, and_comm, ← and_assoc, ←
    disjoint_union_right, diff_union_self, union_eq_self_of_subset_right hI.subset, and_comm, disjoint_comm]

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