bijective₂_of_injective — Mathlib

English

If f is injective and g is surjective and f ∘ g is injective, then f and g are bijective.

Русский

Пусть f инъективна, g сюръективна и f ∘ g инъективна; тогда f и g биективны.

LaTeX

$$$Injective\\,f \\rightarrow Surjective\\,f \\rightarrow (Injective\\,(f \\circ g) \\Rightarrow (Bijective\\,f \\wedge Bijective\\,g))$$$

Lean4

theorem bijective₂_of_injective {g : γ → α} (hf : Surjective f) (hg : Surjective g) (I : Injective (f ∘ g)) :
    Bijective f ∧ Bijective g :=
  ⟨⟨I.of_comp_right hg, hf⟩, I.of_comp, hg⟩

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