Theorems · Theorem · order theory

Set.SurjOn.cancel_right

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β} {g₁ g₂ : β → γ},
  Set.SurjOn f s t → Set.MapsTo f s t → (Set.EqOn (g₁ ∘ f) (g₂ ∘ f) s ↔ Set.EqOn g₁ g₂ t)

Defined in

Mathlib.Data.Set.Function

Cited by

1 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms