surjective_comp

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.surjective_comp

English

Equiv.surjective_comp: For e : α ≃ β and f : β → γ, Surjective (f ∘ e) ↔ Surjective f.

Русский

Для эквивалентности e и функции f верно: Surjective (f ∘ e) ⇔ Surjective f.

LaTeX

$$Surjective\\left( f \\circ e \\right) \\iff Surjective\\left( f \\right)$$

Lean4

theorem surjective_comp (e : α ≃ β) (f : β → γ) : Surjective (f ∘ e) ↔ Surjective f :=
  EquivLike.surjective_comp e f

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

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

Разделы

Аффилиация

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