imageFactorization_surjective

Mathlib.Data.Set.Image

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

English

The map imageFactorization f s : s → image f s is surjective.

Русский

Образ факторизации imageFactorization f s : s → image f s сюръективен.

LaTeX

$$$\\operatorname{Surjective}(\\operatorname{imageFactorization} f s)$$$

Lean4

theorem imageFactorization_surjective {f : α → β} {s : Set α} : Surjective (imageFactorization f s) :=
  fun ⟨_, ⟨a, ha, rfl⟩⟩ => ⟨⟨a, ha⟩, rfl⟩

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

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

Разделы

Аффилиация

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