contractElem_eq_self — Mathlib

English

If a single element e is not in the ground E, contracting {e} leaves M unchanged: if e ∉ E then M / {e} = M.

Русский

Если элемент e не принадлежит грунту E, сокращение по {e} не меняет M: e ∉ E ⇒ M / {e} = M.

LaTeX

$$$ e \\notin E \\Rightarrow M / \\{e\\} = M $$$

Lean4

theorem contractElem_eq_self (he : e ∉ M.E) : M ／ { e } = M := by
  rw [← dual_delete_dual, deleteElem_eq_self (by simpa), dual_dual]

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