Theorems · Theorem · order theory

Set.LeftInvOn.comp

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β} {g : β → γ} {f' : β → α}
  {g' : γ → β}, Set.LeftInvOn f' f s → Set.LeftInvOn g' g t → Set.MapsTo f s t → Set.LeftInvOn (f' ∘ g') (g ∘ f) s

Defined in

Mathlib.Data.Set.Function

Cited by

2 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms