comp_surjective

Mathlib.Data.FunLike.Equiv

URI: https://scilib.ai/kg/mathlib#EquivLike.comp_surjective

← MathLib Explorer

English

Surjectivity of a composition e ∘ f is equivalent to the surjectivity of f.

Русский

Сюръективность композиции e ∘ f эквивалентна сюръективности f.

LaTeX

$$$\text{Surjective}(e \circ f) \iff \text{Surjective}(f)$$$

Lean4

@[simp]
theorem comp_surjective (f : α → β) (e : F) : Function.Surjective (e ∘ f) ↔ Function.Surjective f :=
  Function.Surjective.of_comp_iff' (EquivLike.bijective e) f

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

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

Разделы

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

Аффилиация

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