to_leftInverse — Mathlib

English

If x is a fixed point of f and g is a left inverse of f (i.e., g ∘ f = id), then x is a fixed point of g.

Русский

Если x является фиксированной точкой f и g является левым обратным к f (g ∘ f = id), тогда x — фиксированная точка g.

LaTeX

$$$f(x)=x \wedge (g\circ f)=\mathrm{id} \Rightarrow g(x)=x$$$

Lean4

/-- If `x` is a fixed point of `f` and `g` is a left inverse of `f`, then `x` is a fixed
point of `g`. -/
theorem to_leftInverse (hf : IsFixedPt f x) (h : LeftInverse g f) : IsFixedPt g x :=
  calc
    g x = g (f x) := congr_arg g hf.symm
    _ = x := h x

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