bijOn_fixedPoints_comp — Mathlib

English

If two maps f and g commute, then f is bijective on the fixed points of f ∘ g, i.e., inverse on those fixed points given by g.

Русский

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

LaTeX

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

Lean4

/-- Given two maps `f : α → β` and `g : β → α`, `g` is a bijective map between the fixed points
of `f ∘ g` and the fixed points of `g ∘ f`. The inverse map is `f`, see `invOn_fixedPoints_comp`. -/
theorem bijOn_fixedPoints_comp (f : α → β) (g : β → α) : Set.BijOn g (fixedPoints <| f ∘ g) (fixedPoints <| g ∘ f) :=
  (invOn_fixedPoints_comp f g).bijOn (mapsTo_fixedPoints_comp g f) (mapsTo_fixedPoints_comp f g)

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