comp_right — Mathlib

English

Equivalent statement of surjectivity vs injectivity for the composition map.

Русский

Эквивалентность сюръективности и инъективности для композиционной карты.

LaTeX

$$$\operatorname{Surjective}(\lambda g: \beta \to \gamma.\ g \circ f) \iff \operatorname{Injective}(f)$$$

Lean4

theorem comp_right (hf : Bijective f) : Bijective fun g : β → γ ↦ g ∘ f :=
  ⟨hf.surjective.injective_comp_right, fun g ↦
    ⟨g ∘ surjInv hf.surjective, by simp only [comp_assoc g _ f, (leftInverse_surjInv hf).comp_eq_id, comp_id]⟩⟩

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