Function.IsFixedPt.eq
theorem Function.IsFixedPt.eq : ∀ {α : Type u} {f : α → α} {x : α}, Function.IsFixedPt f x → f x = x
The theorem `Function.IsFixedPt.eq` states that for any type `α`, any function `f` from `α` to `α`, and any element `x` of `α`, if `x` is a fixed point of the function `f`, then the function `f` applied to `x` equals `x`. In other words, if `x` remains unchanged under the action of `f`, then `f(x) = x`. This theorem can be useful for rewriting or simplification tactics in Lean.
More concisely: If `f` is a function from type `α` to itself and `x` is a fixed point of `f`, then `f(x) = x`.
|
Function.IsFixedPt.iterate
theorem Function.IsFixedPt.iterate :
∀ {α : Type u} {f : α → α} {x : α}, Function.IsFixedPt f x → ∀ (n : ℕ), Function.IsFixedPt f^[n] x
This theorem states that if a point `x` is a fixed point of a function `f` (meaning that applying `f` to `x` yields `x`), then `x` is also a fixed point of the `n`th iterate of `f`. In mathematical terms, if `f(x) = x`, then `f^n(x) = x` for all natural numbers `n`, where `f^n` denotes the function `f` applied `n` times.
More concisely: If `x` is a fixed point of the function `f`, then `x` is also a fixed point of `f^n` for all natural numbers `n`.
|
Function.IsFixedPt.perm_zpow
theorem Function.IsFixedPt.perm_zpow :
∀ {α : Type u} {x : α} {e : Equiv.Perm α}, Function.IsFixedPt (⇑e) x → ∀ (n : ℤ), Function.IsFixedPt (⇑(e ^ n)) x
The theorem `Function.IsFixedPt.perm_zpow` states that for any type `α`, any point `x` of type `α`, and any permutation `e` of type `α`, if `x` is a fixed point of the function represented by the permutation `e` (meaning applying `e` to `x` gives back `x`), then `x` is also a fixed point of the function represented by the `n`-th power of `e` for any integer `n`. In other words, applying the `n`-th power of `e` to `x` also gives back `x`.
More concisely: If `x` is a fixed point of a permutation `e` on type `α`, then `x` is also a fixed point of `e` raised to the power of any integer `n`.
|
Function.IsFixedPt.map
theorem Function.IsFixedPt.map :
∀ {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {x : α},
Function.IsFixedPt fa x → ∀ {g : α → β}, Function.Semiconj g fa fb → Function.IsFixedPt fb (g x)
The theorem `Function.IsFixedPt.map` states that if a function `g` semiconjugates another function `fa` to a function `fb`, then `g` maps the fixed points of `fa` to the fixed points of `fb`. Here, a function `fa` from a type `α` to itself has a fixed point `x` if applying `fa` to `x` results in `x` itself. Similarly, a function `fb` from a type `β` to itself has a fixed point `y` if applying `fb` to `y` results in `y` itself. A function `g` from `α` to `β` semiconjugates `fa` to `fb` if for every `x` in `α`, applying `g` after `fa` to `x` results in the same value as applying `fb` after `g` to `x`.
More concisely: If function `g` semiconjugates `fa` to `fb`, then `g` maps the fixed points of `fa` to the fixed points of `fb`. In other words, for all fixed points `x` of `fa`, `g(x)` is a fixed point of `fb`.
|
Function.Commute.right_bijOn_fixedPoints_comp
theorem Function.Commute.right_bijOn_fixedPoints_comp :
∀ {α : Type u} {f g : α → α},
Function.Commute f g → Set.BijOn g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (f ∘ g))
The theorem `Function.Commute.right_bijOn_fixedPoints_comp` states that for any type `α` and for two self-maps `f` and `g` defined on this type, if `f` and `g` commute (meaning applying `f` after `g` is the same as applying `g` after `f`), then `g` is bijective on the set of fixed points of the composition of `f` and `g`. In other words, when restricted to the fixed points of `f ∘ g`, the map `g` is both injective (no two different points map to the same point) and surjective (every point is the image of some point), making it a bijective function. This theorem is a specific instance of the more general theorem `Function.bijOn_fixedPoints_comp`.
More concisely: If two self-maps `f` and `g` of a type `α` commute, then `g` is a bijection on the fixed points of their composition `f ∘ g`.
|
Function.Semiconj.mapsTo_fixedPoints
theorem Function.Semiconj.mapsTo_fixedPoints :
∀ {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {g : α → β},
Function.Semiconj g fa fb → Set.MapsTo g (Function.fixedPoints fa) (Function.fixedPoints fb)
The theorem `Function.Semiconj.mapsTo_fixedPoints` states that for any types `α` and `β`, and for any functions `fa : α → α`, `fb : β → β`, and `g : α → β`, if `g` semiconjugates `fa` to `fb` (meaning `g` composed with `fa` equals `fb` composed with `g`), then `g` maps the fixed points of `fa` to the fixed points of `fb`. In other words, if an element is a fixed point of `fa` (meaning it remains unchanged when applied to `fa`), then its image under `g` is a fixed point of `fb`.
More concisely: If functions `fa : α → α`, `fb : β → β`, and `g : α → β` satisfy `g ∘ fa = fb ∘ g`, then `g` maps the fixed points of `fa` to the fixed points of `fb`.
|
Function.IsFixedPt.to_leftInverse
theorem Function.IsFixedPt.to_leftInverse :
∀ {α : Type u} {f g : α → α} {x : α}, Function.IsFixedPt f x → Function.LeftInverse g f → Function.IsFixedPt g x
The theorem `Function.IsFixedPt.to_leftInverse` states that for any type `α` and any two functions `f` and `g` from `α` to `α`, and any element `x` of `α`, if `x` is a fixed point of function `f` (i.e., `f(x) = x`) and `g` is a left inverse of `f` (i.e., composing `g` after `f`, `g ∘ f`, gives the identity function), then `x` is also a fixed point of function `g` (i.e., `g(x) = x`).
More concisely: If `x` is a fixed point of `f` and `g` is a left inverse of `f`, then `x` is a fixed point of `g`.
|
Function.bijOn_fixedPoints_comp
theorem Function.bijOn_fixedPoints_comp :
∀ {α : Type u} {β : Type v} (f : α → β) (g : β → α),
Set.BijOn g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (g ∘ f))
The theorem `Function.bijOn_fixedPoints_comp` states that for two given functions `f` and `g` where `f` maps from a type `α` to a type `β` and `g` maps from `β` back to `α`, `g` is a bijective function (both injective and surjective) between the set of fixed points of the composition `f ∘ g` and the set of fixed points of the composition `g ∘ f`. In other words, `g` maps every fixed point of `f ∘ g` to a unique fixed point of `g ∘ f` and covers all the fixed points of `g ∘ f`. The function `f` acts as the inverse map for this bijection.
More concisely: The function `g` is a bijection between the fixed points of `f ∘ g` and the fixed points of `g ∘ f`, with `f` acting as the inverse.
|
Function.Commute.invOn_fixedPoints_comp
theorem Function.Commute.invOn_fixedPoints_comp :
∀ {α : Type u} {f g : α → α},
Function.Commute f g → Set.InvOn f g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (f ∘ g))
The theorem `Function.Commute.invOn_fixedPoints_comp` states that for any type `α` and any pair of self-maps `f` and `g` on `α`, if `f` and `g` commute i.e., `f (g x) = g (f x)` for all `x` in `α`, then `f` and `g` are inverses of each other on the set of fixed points of the composition `f ∘ g`. A fixed point of a function is an element that is unchanged by the function. Thus, this theorem relates the properties of commuting functions and their fixed points under composition.
More concisely: If functions `f` and `g` commute and have a common set of fixed points, then they are inverses on this set.
|
Function.IsFixedPt.comp
theorem Function.IsFixedPt.comp :
∀ {α : Type u} {f g : α → α} {x : α},
Function.IsFixedPt f x → Function.IsFixedPt g x → Function.IsFixedPt (f ∘ g) x
This theorem states that if a point 'x' is a fixed point for two functions 'f' and 'g' (meaning that applying 'f' or 'g' to 'x' leaves 'x' unchanged), then 'x' is also a fixed point for the composition of 'f' and 'g' (denoted as 'f ∘ g'). In other words, applying the function 'f' followed by the function 'g' to the point 'x' also leaves 'x' unchanged.
More concisely: If points $x$ are fixed under both functions $f$ and $g$, then $x$ is a fixed point of their composition $f \circ g$.
|
Function.invOn_fixedPoints_comp
theorem Function.invOn_fixedPoints_comp :
∀ {α : Type u} {β : Type v} (f : α → β) (g : β → α),
Set.InvOn f g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (g ∘ f))
This theorem states that for any two functions `f : α → β` and `g : β → α`, `f` and `g` are inverses of each other when restricted to the sets of fixed points of `f ∘ g` and `g ∘ f` respectively. In other words, for any elements in `α` and `β` that remain unchanged when `f ∘ g` or `g ∘ f` is applied, `f` and `g` will take such elements back to their original values.
More concisely: If functions `f : α → β` and `g : β → α` have the property that `f (g (x)) = x` for all `x` in the fixed points of `f ∘ g`, and `g (f (x)) = x` for all `x` in the fixed points of `g ∘ f`, then `f` and `g` are mutually inverse functions.
|
Function.Commute.left_bijOn_fixedPoints_comp
theorem Function.Commute.left_bijOn_fixedPoints_comp :
∀ {α : Type u} {f g : α → α},
Function.Commute f g → Set.BijOn f (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (f ∘ g))
This theorem states that, for any type `α` and two self-maps `f` and `g` on `α`, if `f` and `g` commute (i.e., applying `f` after `g` is the same as applying `g` after `f` for any element of `α`), then `f` is bijective on the set of fixed points of the composition of `f` and `g`. In other words, `f` is both injective (each element in the domain maps to a unique element in the codomain) and surjective (every element in the codomain is the image of some element in the domain) when restricted to the set of elements that remain unchanged when `f ∘ g` is applied to them. This is a specialized case of the theorem `Function.bijOn_fixedPoints_comp`.
More concisely: If two self-maps `f` and `g` on a type `α` commute and have the same fixed points, then `f` is a bijection on the set of fixed points.
|
Function.isFixedPt_id
theorem Function.isFixedPt_id : ∀ {α : Type u} (x : α), Function.IsFixedPt id x
The theorem `Function.isFixedPt_id` states that for every type `α` and for every point `x` of type `α`, `x` is a fixed point of the identity function `id`. In other words, applying the identity function to any point `x` will always return `x`, which is the definition of a fixed point according to `Function.IsFixedPt`. This is a fundamental property of the identity function in mathematics, conveyed as $\forall x \in \alpha, id(x) = x$.
More concisely: For all types `α` and points `x` of type `α`, the identity function `id` maps `x` to a fixed point `x`. In Lean: `Function.isFixedPt id x`.
|
Function.mapsTo_fixedPoints_comp
theorem Function.mapsTo_fixedPoints_comp :
∀ {α : Type u} {β : Type v} (f : α → β) (g : β → α),
Set.MapsTo f (Function.fixedPoints (g ∘ f)) (Function.fixedPoints (f ∘ g))
The theorem `Function.mapsTo_fixedPoints_comp` states that for any function `f` mapping from a type `α` to a type `β`, and any function `g` mapping from type `β` to type `α`, `f` maps the set of fixed points of the composition `g ∘ f` to the set of fixed points of the composition `f ∘ g`. In other words, if an element is a fixed point for the function `g ∘ f` (i.e., applying `g ∘ f` leaves the element unchanged), then its image under `f` is a fixed point for the function `f ∘ g` (i.e., applying `f ∘ g` to the image leaves this image unchanged).
More concisely: If `g ∘ f` and `f ∘ g` have a common fixed point, then `g(fixed_point_of g ∘ f)` is a fixed point of `f circ g`.
|
Function.IsFixedPt.left_of_comp
theorem Function.IsFixedPt.left_of_comp :
∀ {α : Type u} {f g : α → α} {x : α},
Function.IsFixedPt (f ∘ g) x → Function.IsFixedPt g x → Function.IsFixedPt f x
The theorem states that for any type `α` and functions `f` and `g` of type `α → α`, if a point `x` of type `α` is a fixed point of both the composition `f ∘ g` and `g`, then `x` is also a fixed point of `f`. In simple terms, if applying the function `f` after `g` to `x` yields `x` itself, and applying `g` to `x` also yields `x`, then applying `f` to `x` must yield `x` too.
More concisely: If `x` is a fixed point of both `f` and `g` such that `g(x) = x` and `(f ∘ g)(x) = x`, then `f(x) = x`.
|