contractElem_indep_iff — Mathlib

English

If e is a nonloop in M, then (M / {e}).Indep I holds iff e ∉ I and M.Indep(I ∪ {e}).

Русский

Если e не является петлей в M, то (M / {e}).Indep I равно истинному, если и только если e не принадлежит I и M независим по I ∪ {e}.

LaTeX

$$$ (M / \{e\}).Indep I \Leftrightarrow (e \notin I) \land M.Indep(I \cup \{e\}) $$$

Lean4

theorem contractElem_indep_iff (he : M.IsNonloop e) : (M ／ { e }).Indep I ↔ e ∉ I ∧ M.Indep (insert e I) := by
  simp [he.indep.contract_indep_iff]

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