sumMap — Mathlib

English

Let f: α → β and g: α' → β' be surjective. Then the induced map Sum.map f g : α ⊕ α' → β ⊕ β' is surjective.

Русский

Пусть f: α → β и g: α' → β' сюръективны. Тогда отображение Sum.map f g: α ⊕ α' → β ⊕ β' сюръективно.

LaTeX

$$$\big(\operatorname{Surjective} f\big) \land \big(\operatorname{Surjective} g\big) \;\Rightarrow\; \operatorname{Surjective}(\mathrm{Sum.map}\, f\, g).$$$

Lean4

theorem sumMap {f : α → β} {g : α' → β'} (hf : Surjective f) (hg : Surjective g) : Surjective (Sum.map f g)
  | inl y =>
    let ⟨x, hx⟩ := hf y
    ⟨inl x, congr_arg inl hx⟩
  | inr y =>
    let ⟨x, hx⟩ := hg y
    ⟨inr x, congr_arg inr hx⟩

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