erase_injOn — Mathlib

English

Removing a from s behaves injectively on s: if s.erase a = s.erase b for a,b ∈ s, then a = b.

Русский

Удаление элемента из множества s действует инъективно на s: если s.erase a = s.erase b для a,b ∈ s, то a = b.

LaTeX

$$$\\forall a,b \\in s:\\ s\\setminus \\{a\\} = s\\setminus \\{b\\} \\Rightarrow a=b$$$

Lean4

theorem erase_injOn (s : Finset α) : Set.InjOn s.erase s := fun _ _ _ _ => (erase_inj s ‹_›).mp

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