insert_inj_on'

Mathlib.Data.Finset.BooleanAlgebra

URI: https://scilib.ai/kg/mathlib#Finset.insert_inj_on'

English

The map a ↦ insert a s is injective on the complement sᶜ.

Русский

Отображение a ↦ s ∪ {a} инъективно на дополнении к s.

LaTeX

$$$\\mathrm{InjOn}\\ (\\lambda a. s \\cup \\{a\\})\\ (s^{c})$$$

Lean4

theorem insert_inj_on' (s : Finset α) : Set.InjOn (fun a => insert a s) (sᶜ : Finset α) :=
  by
  rw [coe_compl]
  exact s.insert_inj_on

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

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

Разделы

Аффилиация

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