contract_dep_iff — Mathlib

English

The Dep statement after contraction reduces to Disjoint and Dep on union with I.

Русский

Зависимость после сокращения сводится к несовпадению и зависимости по объединению с I.

LaTeX

$$$ (M ／ X).Dep D \iff M.Dep(D ∪ I) ∧ Disjoint X D $$$

Lean4

theorem contract_dep_iff (hI : M.IsBasis I X) {D : Set α} : (M ／ X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D :=
  hI.isBasis'.contract_dep_iff

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