comp_surjective

Mathlib.Logic.Equiv.Defs

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

English

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

Русский

Для f : α → β и e : β ≃ γ, Surjective (e ∘ f) ⇔ Surjective f.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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