image_univ_equiv

Mathlib.Data.Finset.BooleanAlgebra

URI: https://scilib.ai/kg/mathlib#Finset.image_univ_equiv

English

For f : β ≃ α, the image of the universe under f is the universe: univ.image f = univ.

Русский

Для биективного отображения f : β ≃ α образ вселенной равен вселенной.

LaTeX

$$$ univ.image f = univ $$$

Lean4

@[simp]
theorem image_univ_equiv [Fintype β] (f : β ≃ α) : univ.image f = univ :=
  Finset.image_univ_of_surjective f.surjective

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

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

Разделы

Аффилиация

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