Theorems · Definition · logic and foundations

Quot.map

{α : Sort u_1} →
  {β : Sort u_2} →
    {ra : α → α → Prop} → {rb : β → β → Prop} → (f : α → β) → (∀ ⦃a b : α⦄, ra a b → rb (f a) (f b)) → Quot ra → Quot rb

Map a function f : α → β such that ra x y implies rb (f x) (f y) to a map Quot ra → Quot rb.

Defined in

Mathlib.Data.Quot

Cited by

5 results in Mathlib

Foundations

Depth 4 from the axioms · uses Quot.sound