of_leftInverse — Mathlib

English

If a map g has a left inverse to f (g is a left inverse of f) and f x is a unit, then x is a unit.

Русский

Если g имеет левую обратную связь к f (g является левым обратным к f) и f(x) — единица, тогда x — единица.

LaTeX

$$$\\text{LeftInverse}(g,f) \\Rightarrow (\\text{IsUnit}(f(x)) \\Rightarrow \\text{IsUnit}(x)).$$$

Lean4

@[to_additive]
theorem of_leftInverse [MonoidHomClass G N M] {f : F} {x : M} (g : G) (hfg : Function.LeftInverse g f)
    (h : IsUnit (f x)) : IsUnit x := by simpa only [hfg x] using h.map g

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