Theorems · Theorem · order theory

Set.SurjOn.invOn_invFunOn

∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} [inst : Nonempty α],
  Set.SurjOn f s t → Set.InvOn (Function.invFunOn f s) f (Function.invFunOn f s '' t) t

Defined in

Mathlib.Data.Set.Function

Cited by

1 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Nonempty