image_compl

Mathlib.Logic.Equiv.Set

URI: https://scilib.ai/kg/mathlib#Equiv.image_compl

English

Let e be a bijection. The image of the complement of S equals the complement of the image of S.

Русский

Пусть e — биекция. Образ дополнения S равен дополнению образа S.

LaTeX

$$$ e[S^c] = (e[S])^c $$$

Lean4

protected theorem image_compl {α β} (f : Equiv α β) (s : Set α) : f '' sᶜ = (f '' s)ᶜ :=
  image_compl_eq f.bijective

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

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

Разделы

Аффилиация

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