mk — Mathlib · SciLib

English

If f maps s to t, is injective on s, and is surjective on s to t, then f is bijective on s to t.

Русский

Если f отображает s в t, инъективна на s и сюръективна на s, тогда f — биекция на s к t.

LaTeX

$$$ \mathrm{MapsTo} f s t \land \mathrm{InjOn} f s \land \mathrm{SurjOn} f s t \rightarrow \mathrm{BijOn} f s t $$$

Lean4

theorem mk (h₁ : MapsTo f s t) (h₂ : InjOn f s) (h₃ : SurjOn f s t) : BijOn f s t :=
  ⟨h₁, h₂, h₃⟩

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