Theorems · Theorem · order theory

Set.BijOn.sdiff_singleton

∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {a : α},
  Set.BijOn f s t → a ∈ s → Set.BijOn f (s \ {a}) (t \ {f a})

Defined in

Mathlib.Data.Set.Function

Cited by

0 results in Mathlib

Foundations

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