injective_iff_surjective_of_equiv

English

For f: α → β and an equivalence e: α ≃ β, Injective f is equivalent to Surjective f.

Русский

Для f: α → β и эквиваленции e: α ≃ β, инъективность f эквивалентна сюръективности f.

LaTeX

$$$\\operatorname{Injective}(f) \\iff \\operatorname{Surjective}(f)$$$

Lean4

theorem injective_iff_surjective_of_equiv {f : α → β} (e : α ≃ β) : Injective f ↔ Surjective f :=
  have : Injective (e.symm ∘ f) ↔ Surjective (e.symm ∘ f) := injective_iff_surjective
  ⟨fun hinj => by simpa [Function.comp] using e.surjective.comp (this.1 (e.symm.injective.comp hinj)), fun hsurj => by
    simpa [Function.comp] using e.injective.comp (this.2 (e.symm.surjective.comp hsurj))⟩

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