comp — Mathlib

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

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