Theorems · Theorem · dynamical systems

Function.invOn_fixedPoints_comp

∀ {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α),
  Set.InvOn f g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (g ∘ f))

Any two maps f : α → β and g : β → α are inverse of each other on the sets of fixed points of f ∘ g and g ∘ f, respectively.

Defined in

Mathlib.Dynamics.FixedPoints.Basic

Cited by

2 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms