erase_injOn' — Mathlib

English

For a fixed a, the map s ↦ erase s a is injective on the family of Finsets containing a.

Русский

Для фиксированного a отображение s ↦ erase s a инъективно на множестве Finset α с условием a ∈ s.

LaTeX

$$$ \\forall a : \\alpha, (\\{s : Finset \\alpha | a \\in s\\}).InjOn (fun s => erase\\ s\\ a)$$$

Lean4

theorem erase_injOn' (a : α) : {s : Finset α | a ∈ s}.InjOn fun s => erase s a := fun s hs t ht (h : s.erase a = _) =>
  by rw [← insert_erase hs, ← insert_erase ht, h]

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