quotientKerEquivOfRightInverse — Mathlib

English

If f has a computable right-inverse g, then the quotient by ker f is equivalent to β.

Русский

Если у f есть вычислимый правый обратный g, то фактор-множество по ker f эквивалентно β.

LaTeX

$$$$ Quotient(\\ker f) \\simeq β. $$$$

Lean4

/-- If `f` has a computable right-inverse, then the quotient by its kernel is equivalent to its
domain. -/
@[simps]
def quotientKerEquivOfRightInverse (g : β → α) (hf : Function.RightInverse g f) : Quotient (ker f) ≃ β
    where
  toFun a := (Quotient.liftOn' a f) fun _ _ => id
  invFun b := Quotient.mk'' (g b)
  left_inv a := Quotient.inductionOn' a fun a => Quotient.sound' <| hf (f a)
  right_inv := hf

Похожие утверждения