invOn_fixedPoints_comp — Mathlib

English

If f and g commute, then f and g form an inverse pair on fixed points of f ∘ g; this is a particular case of a more general bijection between fixed-point sets.

Русский

Если f и g коммутируют, то они образуют пару обратных на фиксированных точках f ∘ g; частный случай общего биективного соответствия между фиксированными точками.

LaTeX

$$$Set.InvOn f g (fixedPoints (f\circ g)) (fixedPoints (g\circ f))$$$

Lean4

/-- If self-maps `f` and `g` commute, then they are inverse of each other on the set of fixed points
of `f ∘ g`. This is a particular case of `Function.invOn_fixedPoints_comp`. -/
theorem invOn_fixedPoints_comp (h : Commute f g) : Set.InvOn f g (fixedPoints <| f ∘ g) (fixedPoints <| f ∘ g) := by
  simpa only [h.comp_eq] using Function.invOn_fixedPoints_comp f g

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