Theorems · Definition · logic and foundations

Set.BijOn

{α : Type u} → {β : Type v} → (α → β) → Set α → Set β → Prop

f is bijective from s to t if f is injective on s and f '' s = t.

Defined in

Mathlib.Data.Set.Operations

Cited by

168 results in Mathlib

Foundations

Depth 7 from the axioms, rests on 19 definitions · uses no axioms