contract_delete_diff — Mathlib

English

Contracting by C and then deleting D is equal to contracting by C and then deleting D \ C: M / C \ D = M / C \ (D \ C).

Русский

Сжатие по C, затем удаление D эквивалентно сжатию по C и удалению D \ C.

LaTeX

$$M / C \\ D = M / C \\ (D \ C)$$

Lean4

theorem contract_delete_diff (M : Matroid α) (C D : Set α) : M ／ C ＼ D = M ／ C ＼ (D \ C) := by
  rw [delete_eq_delete_iff, contract_ground, diff_eq, diff_eq, ← inter_inter_distrib_right, inter_assoc]

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