Theorems · Definition · logic and foundations

Quotient.map

{α : Sort u_1} →
  {β : Sort u_2} →
    {sa : Setoid α} → {sb : Setoid β} → (f : α → β) → (∀ ⦃a b : α⦄, a ≈ b → f a ≈ f b) → Quotient sa → Quotient sb

Map a function f : α → β that sends equivalent elements to equivalent elements to a function Quotient sa → Quotient sb. Useful to define unary operations on quotients.

Defined in

Mathlib.Data.Quot

Cited by

7 results in Mathlib

Foundations

Depth 5 from the axioms · uses Quot.sound