BijOn — Mathlib

English

Let f: α → β, s ⊆ α, t ⊆ β. Then f is bijective from s to t if it maps s into t, is injective on s, and its image on s is exactly t.

Русский

Пусть f: α → β, s ⊆ α, t ⊆ β. Тогда f является биекцией с s на t, если f[ s ] ⊆ t, ограничение f на s инъективно, и f[s] = t.

LaTeX

$$$\mathrm{BijOn}(f,s,t) \iff (\operatorname{MapsTo} f\,s\,t) \land \mathrm{InjOn}(f,s) \land \mathrm{SurjOn}(f,s,t)$$$

Lean4

/-- `f` is bijective from `s` to `t` if `f` is injective on `s` and `f '' s = t`. -/
def BijOn (f : α → β) (s : Set α) (t : Set β) : Prop :=
  MapsTo f s t ∧ InjOn f s ∧ SurjOn f s t

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