insert_diff_self_of_notMem — Mathlib

English

Insert a and remove a by {a} are inverse on the corresponding domains.

Русский

Операции вставки элемента и удаления по нему обратны на соответствующих множествах.

LaTeX

$$$ \\text{InvOn}(\\text{insert } a,\\, s \\mapsto s \\setminus \\{a\\},\\, \\{s \\mid a \\in s\\},\\, \\{s \\mid a \\notin s\\}) $$$

Lean4

theorem insert_diff_self_of_notMem (h : a ∉ s) : insert a s \ { a } = s := by ext x;
  simp [and_iff_left_of_imp (ne_of_mem_of_not_mem · h)]

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