Function.Semiconj.comp_left
theorem Function.Semiconj.comp_left :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {fab : α → β} {fbc : β → γ} {ga : α → α} {gb : β → β} {gc : γ → γ},
Function.Semiconj fbc gb gc → Function.Semiconj fab ga gb → Function.Semiconj (fbc ∘ fab) ga gc
The theorem `Function.Semiconj.comp_left` asserts that if a function `fbc` from type `β` to `γ` semiconjugates another function `gb` to `gc`, and a function `fab` from type `α` to `β` semiconjugates another function `ga` to `gb`, then the composition of `fbc` and `fab` semiconjugates `ga` to `gc`. In other words, if for all `x`, `fbc(gb(x))` equals `gc(fbc(x))` and `fab(ga(x))` equals `gb(fab(x))`, then for all `x`, `(fbc ∘ fab)(ga(x))` equals `gc((fbc ∘ fab)(x))`.
More concisely: If functions `fbc: β → γ`, `gb: α → β`, `gc: α → γ`, `fab: α → β`, and `ga: α → α` satisfy `gb ∘ fab = fab ∘ ga` and `fbc ∘ gb = gc ∘ fbc`, then `(fbc ∘ fab) = gc ∘ (fab ∘ ga)`.
|
Function.Semiconj.comp_eq
theorem Function.Semiconj.comp_eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β},
Function.Semiconj f ga gb → f ∘ ga = gb ∘ f
The theorem `Function.Semiconj.comp_eq` states that for any types `α` and `β`, and any functions `f : α → β`, `ga : α → α`, and `gb : β → β`, if `f` semiconjugates `ga` to `gb` (i.e., for all `x` in `α`, `f(ga(x))` equals `gb(f(x))`), then the composition `f ∘ ga` equals the composition `gb ∘ f`. This theorem provides a definition of semiconjugation in terms of functional equality.
More concisely: If functions `f : α → β`, `ga : α → α`, and `gb : β → β` satisfy `f (ga x) = gb (f x)` for all `x` in `α`, then `f ∘ ga = gb ∘ f`.
|
Function.semiconj_iff_comp_eq
theorem Function.semiconj_iff_comp_eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β},
Function.Semiconj f ga gb ↔ f ∘ ga = gb ∘ f
The theorem `Function.semiconj_iff_comp_eq` states that for any two types `α` and `β`, and any functions `f : α → β`, `ga : α → α`, `gb : β → β`, the function `f` semiconjugates `ga` to `gb` (in the sense defined by `Function.Semiconj`) if and only if the composition `f ∘ ga` is equal to the composition `gb ∘ f`. In mathematical terms, this theorem confirms that we can equivalently define semiconjugation of functions either by the condition `f(ga(x)) = gb(f(x))` for all `x`, or by the equality of composite functions `f ∘ ga = gb ∘ f`.
More concisely: For any functions $f : \alpha \to \beta$, $ga : \alpha \to \alpha$, and $gb : \beta \to \beta$, $f$ semiconjugates $ga$ to $gb$ if and only if $f \circ ga = gb \circ f$.
|
Function.Semiconj.eq
theorem Function.Semiconj.eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β},
Function.Semiconj f ga gb → ∀ (x : α), f (ga x) = gb (f x)
The theorem `Function.Semiconj.eq` states that for all types `α` and `β`, and for all functions `f` from `α` to `β`, `ga` from `α` to `α`, and `gb` from `β` to `β`, if `f` semiconjugates `ga` to `gb` (that is, if the composition `f` after `ga` is equivalent to the composition `gb` after `f`), then for every element `x` of type `α`, the application of `f` to `ga` of `x` is equal to `gb` of `f` of `x`. In mathematical terms, if $f \circ ga = gb \circ f$, then for all $x$ in $\alpha$, $f(ga(x)) = gb(f(x))$.
More concisely: If functions $f: \alpha \to \beta$, $ga: \alpha \to \alpha$, and $gb: \beta \to \beta$ satisfy $f \circ ga = gb \circ f$, then for all $x \in \alpha$, $f(ga(x)) = gb(f(x))$.
|
Function.Semiconj.option_map
theorem Function.Semiconj.option_map :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β},
Function.Semiconj f ga gb → Function.Semiconj (Option.map f) (Option.map ga) (Option.map gb)
This theorem states that if a function `f` from type `α` to type `β` semiconjugates a function `ga` from `α` to `α` to a function `gb` from `β` to `β` (meaning that for every element `x` of type `α`, applying `f` to the result of `ga(x)` is the same as applying `gb` to the result of `f(x)`), then the function `Option.map f` semiconjugates `Option.map ga` to `Option.map gb`. In other words, the "semiconjugating" property of a function `f` is preserved when we extend `f`, `ga`, and `gb` to operate on optional values.
More concisely: If function `f` semiconjugates `ga` to `gb`, then `Option.map f` semiconjugates `Option.map ga` to `Option.map gb`.
|
Function.Semiconj₂.eq
theorem Function.Semiconj₂.eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β},
Function.Semiconj₂ f ga gb → ∀ (x y : α), f (ga x y) = gb (f x) (f y)
The theorem `Function.Semiconj₂.eq` states that for any types `α` and `β`, any function `f : α → β`, and any two binary operations `ga : α → α → α` and `gb : β → β → β`, if `f` semiconjugates `ga` to `gb` (meaning for all `x` and `y` in `α`, the function `f` applied on the operation `ga` on `x` and `y` equals the operation `gb` on `f x` and `f y`), then for any two elements `x` and `y` in `α`, the function `f` applied to the operation `ga` on `x` and `y` indeed equals the operation `gb` on `f x` and `f y`. This is the defining property of semiconjugates.
More concisely: If a function `f` semiconjugs binary operations `ga` and `gb` on types `α` and `β` respectively, then `f (ga x y) = gb (f x) (f y)` for all `x, y` in `α`.
|
Function.Commute.semiconj
theorem Function.Commute.semiconj : ∀ {α : Type u_1} {f g : α → α}, Function.Commute f g → Function.Semiconj f g g := by
sorry
The theorem `Function.Commute.semiconj` states that for any type `α` and any two functions `f` and `g`, both defined on the set `α`, if `f` and `g` commute (meaning, applying `f` after `g` is equivalent to applying `g` after `f`), then `f` semiconjugates `g` to `g` (which means, applying `f` to the result of `g` is equivalent to applying `g` to the result of `f`). These two conditions are technically identical, but are referred to differently when using dot notation in Lean 4.
More concisely: If functions `f` and `g` on type `α` commute, then `f` semiconjugates `g`, i.e., `f ∘ g = g ∘ f`.
|
Function.Semiconj.id_right
theorem Function.Semiconj.id_right : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Semiconj f id id
The theorem `Function.Semiconj.id_right` states that for any function `f` from a type `α` to another type `β`, the function `f` semiconjugates the identity function on `α` to the identity function on `β`. In other words, for any function `f` and any element `x` in `α`, applying `f` to `x` (after applying the identity function to `x`) is the same as applying the identity function to `f(x)`. This theorem essentially establishes that every function commutes with the identity function in the context of semiconjugation.
More concisely: For any function f from type α to type β, the identity function on α semiconjugates to the identity function on β through f.
|
Function.Commute.symm
theorem Function.Commute.symm : ∀ {α : Type u_1} {f g : α → α}, Function.Commute f g → Function.Commute g f
The theorem `Function.Commute.symm` states that for any type `α` and any two functions `f` and `g` from `α` to `α`, if `f` and `g` commute, then `g` and `f` also commute. In other words, if the function composition `f(g(x))` equals `g(f(x))` for all `x` in `α`, then the function composition `g(f(x))` also equals `f(g(x))` for all `x` in `α`. This is the commutativity property of function composition.
More concisely: If functions `f` and `g` from type `α` to `α` commute, that is, `f(g(x)) = g(f(x))` for all `x` in `α`, then they are interchangeable in function composition, i.e., `g(f(x)) = f(g(x))` for all `x` in `α`.
|
Function.Semiconj.inverses_right
theorem Function.Semiconj.inverses_right :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga ga' : α → α} {gb gb' : β → β},
Function.Semiconj f ga gb →
Function.RightInverse ga' ga → Function.LeftInverse gb' gb → Function.Semiconj f ga' gb'
The theorem `Function.Semiconj.inverses_right` states that if a function `f` from type `α` to `β` semiconjugates a function `ga` from `α` to `α` to a function `gb` from `β` to `β` (i.e., `f` composed with `ga` is equivalent to `gb` composed with `f`), and if there exists a function `ga'` that is a right inverse to `ga` (i.e., `ga` composed with `ga'` gives the identity function on `α`) and a function `gb'` that is a left inverse to `gb` (i.e., `gb'` composed with `gb` gives the identity function on `β`), then `f` also semiconjugates `ga'` to `gb'`.
More concisely: If functions `f: α → β`, `ga: α → α`, `gb: β → β`, `ga' : α → α`, and `gb' : β → β` satisfy `f ∘ ga ≈gb ∘ f`, `ga ∘ ga' = id α`, and `gb' ∘ gb = id β`, then `f ∘ ga' ≈ gb'`.
|
Function.Commute.id_left
theorem Function.Commute.id_left : ∀ {α : Type u_1} {f : α → α}, Function.Commute id f
This theorem states that the identity function commutes with any self-map. In other words, if `f` is a function mapping elements of an arbitrary type `α` to `α`, then the identity function applied to the result of `f(x)` equals `f` applied to the result of the identity function on `x`, for all `x` in `α`. Using mathematical notation, this is the same as saying for all `x` in `α`, `id(f(x)) = f(id(x))`.
More concisely: For any function `f` from type `α` to `α`, the identity function commutes with `f`, i.e., `id(f(x)) = f(id(x))` for all `x` in `α`.
|
Function.Semiconj.inverse_left
theorem Function.Semiconj.inverse_left :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β} {f' : β → α},
Function.Semiconj f ga gb → Function.LeftInverse f' f → Function.RightInverse f' f → Function.Semiconj f' gb ga
The theorem `Function.Semiconj.inverse_left` states that for any types `α` and `β`, and functions `f : α → β`, `ga : α → α`, `gb : β → β`, and `f' : β → α`, if `f` semiconjugates `ga` to `gb` and `f'` is both a left inverse and a right inverse of `f`, then `f'` semiconjugates `gb` to `ga`. In other words, if applying `f` after `ga` is the same as applying `gb` after `f` for all inputs, and if applying `f'` after `f` or `f` after `f'` returns the original input for all inputs, then applying `f'` after `gb` is the same as applying `ga` after `f'` for all inputs.
More concisely: If functions `f : α → β`, `ga : α → α`, `gb : β → β`, and `f' : β → α` satisfy `f ∘ ga = gb ∘ f`, `f ∘ f' = id_α`, and `f' ∘ f = id_β`, then `f' ∘ gb = ga ∘ f'`.
|
Function.Semiconj.comp_right
theorem Function.Semiconj.comp_right :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga ga' : α → α} {gb gb' : β → β},
Function.Semiconj f ga gb → Function.Semiconj f ga' gb' → Function.Semiconj f (ga ∘ ga') (gb ∘ gb')
The theorem `Function.Semiconj.comp_right` states that if a function `f` semiconjugates `ga` to `gb` and also semiconjugates `ga'` to `gb'`, then `f` also semiconjugates the composition of `ga` and `ga'` to the composition of `gb` and `gb'`. In other words, if for all `x` in the domain, `f(ga(x)) = gb(f(x))` and `f(ga'(x)) = gb'(f(x))` hold true, then `f(ga(ga'(x))) = gb(gb'(f(x)))` will also hold for all `x`.
More concisely: If functions `f`, `ga`, `ga'`, `gb`, and `gb'` are such that `f` semiconjugates `ga` to `gb` and `ga'` to `gb'`, then `f` semiconjugates `ga ∘ ga'` to `gb ∘ gb'`.
|
Function.Semiconj.commute
theorem Function.Semiconj.commute : ∀ {α : Type u_1} {f g : α → α}, Function.Semiconj f g g → Function.Commute f g := by
sorry
This theorem states that for all types `α` and for all functions `f` and `g` from `α` to `α`, if `f` semiconjugates `g` to `g` (i.e., `f` composed with `g` is equivalent to `g` composed with `f`), then `f` and `g` commute (i.e., the result of applying `f` after `g` to any element is the same as applying `g` after `f` to that element). Essentially, this theorem is saying that semiconjugation of a function to itself is equivalent to the commutation of the function with itself. These two predicates are definitionally equal, but they have different implications when used with dot-notation.
More concisely: If function `f` semiconjugates `g` (i.e., `f ∘ g ≈ g ∘ f`), then `f` and `g` commute (i.e., `f ∘ g = g ∘ f`).
|
Function.Commute.comp_left
theorem Function.Commute.comp_left :
∀ {α : Type u_1} {f f' g : α → α}, Function.Commute f g → Function.Commute f' g → Function.Commute (f ∘ f') g := by
sorry
The theorem `Function.Commute.comp_left` states that for any given type `α` and three functions `f`, `f'`, and `g` that map from `α` to `α`, if `f` commutes with `g` and `f'` commutes with `g`, then the composition of `f` and `f'` also commutes with `g`. In other words, if applying `g` after `f` or `f'` is the same as applying `f` or `f'` after `g`, then applying `g` after the composition of `f` and `f'` is the same as applying the composition of `f` and `f'` after `g`.
More concisely: If functions `f`, `f'`, and `g` map from type `α` to `α`, and `f` commutes with `g` and `f'` commutes with `g`, then `(f' ∘ f)` commutes with `g`, i.e., `g ∘ (f' ∘ f) = (g ∘ f') ∘ f`.
|
Function.Semiconj.trans
theorem Function.Semiconj.trans :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {fab : α → β} {fbc : β → γ} {ga : α → α} {gb : β → β} {gc : γ → γ},
Function.Semiconj fab ga gb → Function.Semiconj fbc gb gc → Function.Semiconj (fbc ∘ fab) ga gc
The theorem `Function.Semiconj.trans` states that if a function `fab : α → β` semiconjugates another function `ga : α → α` to `gb : β → β`, and a function `fbc : β → γ` semiconjugates `gb` to `gc : γ → γ`, then the composition of `fbc` and `fab` also semiconjugates `ga` to `gc`. In other words, if for all `x` in `α`, `fab (ga x) = gb (fab x)` and `fbc (gb x) = gc (fbc x)` hold, then for all `x` in `α`, `(fbc ∘ fab) (ga x) = gc ((fbc ∘ fab) x)` also holds. This captures a transitivity property of the semiconjugacy relation among functions.
More concisely: If functions `fab : α → β` semiconjugate `ga : α → α` to `gb : β → β`, and `fbc : β → γ` semiconjugates `gb` to `gc : γ → γ`, then `fbc ∘ fab` semiconjugates `ga` to `gc`.
|
Function.Commute.refl
theorem Function.Commute.refl : ∀ {α : Type u_1} (f : α → α), Function.Commute f f
This theorem states that for any function `f` from a type `α` to itself, `f` commutes with itself. In other words, for all `α` in the type `u_1` and any function `f: α → α`, applying `f` after `f` is the same as applying `f` before `f`. Mathematically, this means that for all `x` in `α`, `f(f(x))` equals `f(f(x))`, and in function composition notation, `f ∘ f` equals `f ∘ f`.
More concisely: For any function `f: α --> α`, `f ∘ f` equals `f ∘ f`, i.e., `f` commutes with itself.
|
Function.Semiconj.id_left
theorem Function.Semiconj.id_left : ∀ {α : Type u_1} {ga : α → α}, Function.Semiconj id ga ga
The theorem `Function.Semiconj.id_left` states that for any type `α` and any function `ga : α → α`, the identity function for `α` semiconjugates `ga` to itself. In other words, if you pass any element `x` of type `α` to `ga` and then apply the identity function, you get the same result as if you first apply the identity function to `x` and then pass the result to `ga`. This is a formal statement of the fact that applying the identity function doesn't change the outcome of applying `ga`.
More concisely: For any function `ga : α → α`, the identity function is a semigroup homomorphism from `(α, ga)` to itself. In other words, `id ∘ ga = ga ∘ id`.
|
Function.Commute.comp_right
theorem Function.Commute.comp_right :
∀ {α : Type u_1} {f g g' : α → α}, Function.Commute f g → Function.Commute f g' → Function.Commute f (g ∘ g') := by
sorry
The theorem `Function.Commute.comp_right` states that if a function `f` commutes with two functions `g` and `g'`, then `f` also commutes with the composition of `g` and `g'`. In other words, if for all inputs `x`, `f(g(x)) = g(f(x))` and `f(g'(x)) = g'(f(x))`, then it is also true that `f(g(g'(x))) = g(g'(f(x)))` for all `x`. This theorem applies to functions of any type `α`.
More concisely: If functions `f`, `g`, and `g'` satisfy `f(g(x)) = g(f(x))` and `f(g'(x)) = g'(f(x))` for all `x`, then `f(g(g'(x))) = g(g'(f(x)))`.
|
Function.Commute.option_map
theorem Function.Commute.option_map :
∀ {α : Type u_1} {f g : α → α}, Function.Commute f g → Function.Commute (Option.map f) (Option.map g)
The theorem states that if two functions `f` and `g` commute, i.e., for any input `x`, the output of `f` after `g` is the same as the output of `g` after `f` (expressed as `f(g(x)) = g(f(x))`), then the function `Option.map f` also commutes with `Option.map g`. In other words, when `f` and `g` are applied to the values contained within `Option` structures, the order of application still does not affect the result.
More concisely: If functions `f` and `g` commute, i.e., `f(g(x)) = g(f(x))` for all `x`, then `Option.map f (Option.map g x) = Option.map g (Option.map f x)` for all `Option x`.
|
Function.Commute.id_right
theorem Function.Commute.id_right : ∀ {α : Type u_1} {f : α → α}, Function.Commute f id
The theorem `Function.Commute.id_right` states that for any type `α` and any function `f` that maps `α` to `α`, the function `f` commutes with the identity function. In other words, for any element `x` of type `α`, applying `f` to `x` and then applying the identity function gives the same result as applying the identity function to `x` and then applying `f`. This is expressed mathematically as `f(id(x)) = id(f(x))` for all `x` in `α`.
More concisely: For any function `f` mapping type `α` to itself, `f(id(x)) = id(f(x))` holds for all `x` in `α`.
|