restrict_delete_of_disjoint — Mathlib

English

If N ≤_r M and X is disjoint from N.E, then N ≤_r (M \\ X); i.e., restriction is preserved by deleting a disjoint set.

Русский

Если N ≤_r M и X дизъюнктно от N.E, то N ≤_r (M \\ X); то есть ограничение сохраняется после удаления дизъюнктного множества.

LaTeX

$$(N\\le_r M) ∧ Disjoint X N.E) → N \\le_r (M\\setminus X)$$

Lean4

theorem restrict_delete_of_disjoint (h : N ≤r M) (hX : Disjoint X N.E) : N ≤r (M ＼ X) :=
  by
  obtain ⟨D, hD, rfl⟩ := isRestriction_iff_exists_eq_delete.1 h
  refine isRestriction_iff_exists_eq_delete.2 ⟨D \ X, diff_subset_diff_left hD, ?_⟩
  rwa [delete_delete, union_diff_self, union_comm, ← delete_delete, eq_comm, delete_eq_self_iff]

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