bijective₂_of_surjective — Mathlib

English

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

Русский

Если f и g инъективны и f ∘ g сюръективна, тогда f и g биективны.

LaTeX

$$$(\\text{Injective }f) \\rightarrow (\\text{Injective }g) \\rightarrow (\\text{Surjective }(f \\circ g)) \\rightarrow (\\text{Bijective }f \\wedge \\text{Bijective }g)$$$

Lean4

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

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