Injection_is_Bijection_iff_Inverse_is_Injection

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

bijectioninjectionproofwikiset-theory

Let $\phi: S \to T$ be an injection. Then $\phi$ is a bijection its inverse $\phi^{-1}$ is also an injection.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Injection_is_Bijection_iff_Inverse_is_Injection {S T : Type _} (f : S → T) (hf : Function.Injective f) : Function.Bijective f ↔ Function.Surjective f := by sorry

Source

https://proofwiki.org/wiki/Injection_is_Bijection_iff_Inverse_is_Injection

View graph