map_univ_of_surjective

Mathlib.Data.Finset.BooleanAlgebra

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

← MathLib Explorer

English

If f : α → β is surjective, then univ.map f = univ.

Русский

Если отображение f : α → β сюръективно, то образ вселенной равен вселенной.

LaTeX

$$$ univ.map f = univ $$$

Lean4

theorem map_univ_of_surjective [Fintype β] {f : β ↪ α} (hf : Surjective f) : univ.map f = univ :=
  eq_univ_of_forall <| hf.forall.2 fun _ => mem_map_of_mem _ <| mem_univ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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