surjective_comp_right

Mathlib.Logic.Function.Basic

URI: https://scilib.ai/kg/mathlib#Function.Injective.surjective_comp_right

← MathLib Explorer

English

If γ is nonempty, the map g ↦ g ∘ f is surjective.

Русский

При непустом γ отображение g ↦ g ∘ f сюръективно.

LaTeX

$$$\operatorname{Surjective}(\lambda g: \beta \to \gamma.\ g \circ f)$ $$

Lean4

theorem surjective_comp_right [Nonempty γ] (hf : Injective f) : Surjective fun g : β → γ ↦ g ∘ f :=
  hf.surjective_comp_right' fun _ ↦ Classical.choice ‹_›

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

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

Разделы

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

Аффилиация

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