right_bijOn_fixedPoints_comp — Mathlib

English

If two maps commute, then g is bijective on the fixed points of f ∘ g; this is a counterpart to the left-bijective case.

Русский

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

LaTeX

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

Lean4

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

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