image_univ_of_surjective

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.image_univ_of_surjective

English

If f is surjective, the image of the entire domain equals the codomain: f'' univ = univ.

Русский

Если отображение сюръективно, образ всей области совпадает с кодоменой: f'' univ = univ.

LaTeX

$$$ f'' \\operatorname{univ} = \\operatorname{univ}. $$$

Lean4

theorem image_univ_of_surjective {ι : Type*} {f : ι → β} (H : Surjective f) : f '' univ = univ :=
  eq_univ_of_forall <| by simpa [image]

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

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

Разделы

Аффилиация

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