erase_inj — Mathlib

English

If removing x from s equals removing y from s for a finite set s, and x is an element of s, then x = y. Conversely, if x = y, removing x and y gives the same set.

Русский

Если из множества s удалить x и получить то же множество, что и удаление y, причём x принадлежит s, то x = y. И наоборот, если x = y, то результаты удаления совпадают.

LaTeX

$$$s\\setminus \\{x\\} = s\\setminus \\{y\\} \\iff x = y \\quad\\text{(при } x \\in s\\text{)}$$$

Lean4

theorem erase_inj {x y : α} (s : Finset α) (hx : x ∈ s) : s.erase x = s.erase y ↔ x = y := by
  grind [eq_of_mem_of_notMem_erase]

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