Theorems · Definition · order theory

Setoid.mapOfSurjective

{α : Type u_1} → {β : Type u_2} → (r : Setoid α) → (f : α → β) → Setoid.ker f ≤ r → Function.Surjective f → Setoid β

Given a surjective function f whose kernel is contained in an equivalence relation r, the equivalence relation on f's codomain defined by x ≈ y ↔ the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by r.

Defined in

Mathlib.Data.Setoid.Basic

Cited by

1 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms