comp — Mathlib

English

Injectivity on a set implies a bijection with its image.

Русский

Инъективность на множестве порождает биекцию между множеством и его образом.

LaTeX

$$$\\text{InjOn}(f,s) \\Rightarrow \\text{BijOn}(f,s,\\operatorname{image} f s)$$$

Lean4

theorem comp (hg : BijOn g t p) (hf : BijOn f s t) : BijOn (g ∘ f) s p :=
  BijOn.mk (hg.mapsTo.comp hf.mapsTo) (hg.injOn.comp hf.injOn hf.mapsTo) (hg.surjOn.comp hf.surjOn)

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