mapsTo_fixedPoints_comp — Mathlib

English

If f and g commute, then f is bijective on fixed points of f ∘ g, i.e., it is invertible there with g providing the inverse.

Русский

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

LaTeX

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

Lean4

/-- Any map `f` sends fixed points of `g ∘ f` to fixed points of `f ∘ g`. -/
theorem mapsTo_fixedPoints_comp (f : α → β) (g : β → α) : Set.MapsTo f (fixedPoints <| g ∘ f) (fixedPoints <| f ∘ g) :=
  fun _ hx => hx.map fun _ => rfl

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