exists_eq_contract_delete_disjoint

English

If N is a minor of M, there exist C, D disjoint with parts of E(M) such that N = M contracted by C and then deleted by D.

Русский

Если N является минором M, существуют пара C, D раздельных по E(M), такие что N = M сокращённый по C и удалённый по D.

LaTeX

$$$ \exists C \subseteq M.E, \exists D \subseteq M.E, Disjoint(C,D) \land N = M/\!C \\ D $$$

Lean4

theorem exists_eq_contract_delete_disjoint (h : N ≤m M) :
    ∃ (C D : Set α), C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D :=
  by
  obtain ⟨C, D, rfl⟩ := h
  exact
    ⟨C ∩ M.E, (D ∩ M.E) \ C, inter_subset_right, diff_subset.trans inter_subset_right,
      disjoint_sdiff_right.mono_left inter_subset_left, by simp [delete_eq_delete_iff, inter_assoc, inter_diff_assoc]⟩

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