surjective_comp_left_iff — Mathlib

English

For nonempty α, Surjective (g ∘ ·) is equivalent to Surjective g.

Русский

Для ненулевого α эквивалентно: сюръективна g ∘ · ровно как сюръективна g.

LaTeX

$$$ [\text{Nonempty } \alpha] \; \text{Surjective}((g \circ \cdot) : (\alpha \to \beta) \to (\alpha \to \gamma)) \; \leftrightarrow \; \text{Surjective}(g) $$$

Lean4

theorem surjective_comp_left_iff [Nonempty α] {g : β → γ} : Surjective (g ∘ · : (α → β) → α → γ) ↔ Surjective g :=
  by
  refine ⟨fun h c ↦ Nonempty.elim ‹_› fun a ↦ ?_, (·.comp_left)⟩
  have ⟨f, hf⟩ := h fun _ ↦ c
  exact ⟨f a, congr_fun hf _⟩

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