Theorems · Theorem · order theory

Function.Semiconj.injOn_preimage

∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β},
  Function.Semiconj f fa fb → ∀ {s : Set β}, Set.InjOn fb s → Set.InjOn f (f ⁻¹' s) → Set.InjOn fa (f ⁻¹' s)

Defined in

Mathlib.Data.Set.Function

Cited by

0 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms