isRestriction_deleteElem — Mathlib

English

If N ≤_r M and e ∉ N.E, then N ≤_r M \\ {e} (i.e., deleting an element not in N does not affect the restriction).

Русский

Если N ≤_r M и e ∉ N.E, тогда N ≤_r M \\ {e}. (удаление элемента, отсутствующего в N, не влияет на ограничение).

LaTeX

$$(N ≤_r M) ∧ (e ∉ N.E) → N ≤_r (M \\ {e})$$

Lean4

theorem isRestriction_deleteElem (h : N ≤r M) (he : e ∉ N.E) : N ≤r M ＼ { e } :=
  h.restrict_delete_of_disjoint (by simpa)

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