left_bijOn_fixedPoints_comp — Mathlib

English

If two maps f and g commute, then f is bijective on the fixed points of f ∘ g; this is a specialized case of a general statement about fixed points under composition.

Русский

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

LaTeX

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

Lean4

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

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