left_of_comp — Mathlib

English

If x is a fixed point of f ∘ g and x is a fixed point of g, then x is a fixed point of f.

Русский

Если x является фиксированной точкой композиции f ∘ g и фиксированной точкой g, то x является фиксированной точкой f.

LaTeX

$$$(f\circ g)(x)=x \quad\text{и}\quad g(x)=x \Rightarrow f(x)=x$$$

Lean4

/-- If `x` is a fixed point of `f ∘ g` and `g`, then it is a fixed point of `f`. -/
theorem left_of_comp (hfg : IsFixedPt (f ∘ g) x) (hg : IsFixedPt g x) : IsFixedPt f x :=
  calc
    f x = f (g x) := congr_arg f hg.symm
    _ = x := hfg

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