insert_injOn

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Function.insert_injOn

English

For a fixed set s, the function a ↦ insert a s is injective on the complement of s.

Русский

Для заданного множества s функция a ↦ insert a s инъективна на комплементе s.

LaTeX

$$$ \\operatorname{InjOn} (\\lambda a \\;\\text{insert}(a,s)) (s^c). $$$

Lean4

theorem insert_injOn (s : Set α) : sᶜ.InjOn fun a => insert a s := fun _a ha _ _ => (insert_inj ha).1

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru