Theorems · Definition · order theory

Setoid.quotientKerEquivOfRightInverse

{α : Type u_1} → {β : Type u_2} → (f : α → β) → (g : β → α) → Function.RightInverse g f → Quotient (Setoid.ker f) ≃ β

If f has a computable right-inverse, then the quotient by its kernel is equivalent to its domain.

Defined in

Mathlib.Data.Setoid.Basic

Cited by

2 results in Mathlib

Foundations

Depth 10 from the axioms · uses Quot.sound