map_surjective — Mathlib

English

Let f: α → γ and g: β → δ be surjective. Then Sum.map f g: α ⊕ β → γ ⊕ δ is surjective.

Русский

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

LaTeX

$$Surjective( Sum.map f g ) ⇔ Surjective f ∧ Surjective g$$

Lean4

@[simp]
theorem map_surjective {f : α → γ} {g : β → δ} : Surjective (Sum.map f g) ↔ Surjective f ∧ Surjective g
    where
  mp
    h :=
    ⟨(fun c => by
        obtain ⟨a | b, h⟩ := h (inl c)
        · exact ⟨a, inl_injective h⟩
        · cases h),
      (fun d => by
        obtain ⟨a | b, h⟩ := h (inr d)
        · cases h
        · exact ⟨b, inr_injective h⟩)⟩
  mpr
    | ⟨hf, hg⟩ => hf.sumMap hg

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