Theorems · Theorem · order theory

Set.BijOn.subset_left

∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {r : Set α},
  Set.BijOn f s t → r ⊆ s → Set.BijOn f r (f '' r)

Defined in

Mathlib.Data.Set.Function

Cited by

1 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms