English
If x is a fixed point of f and g, then x is a fixed point of f ∘ g.
Русский
Если x — фиксированная точка f и g, то x — фиксированная точка f ∘ g.
LaTeX
$$$\text{IsFixedPt } f x \rightarrow \text{IsFixedPt } g x \rightarrow \text{IsFixedPt } (f \circ g) x$$$
Lean4
/-- If `x` is a fixed point of `f` and `g`, then it is a fixed point of `f ∘ g`. -/
protected theorem comp (hf : IsFixedPt f x) (hg : IsFixedPt g x) : IsFixedPt (f ∘ g) x :=
calc
f (g x) = f x := congr_arg f hg
_ = x := hf