map_univ_equiv

Mathlib.Data.Finset.BooleanAlgebra

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

English

For f : α ≃ β, univ.image f = univ.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem map_univ_equiv [Fintype β] (f : β ≃ α) : univ.map f.toEmbedding = univ :=
  map_univ_of_surjective f.surjective

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

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

Разделы

Аффилиация

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