Theorems · Definition

Function.Semiconj

{α : Type u_1} → {β : Type u_2} → (α → β) → (α → α) → (β → β) → Prop

We say that f : α → β semiconjugates ga : α → α to gb : β → β if f ∘ ga = gb ∘ f. We use ∀ x, f (ga x) = gb (f x) as the definition, so given h : Function.Semiconj f ga gb and a : α, we have h a : f (ga a) = gb (f a) and h.comp_eq : f ∘ ga = gb ∘ f.

Defined in

Mathlib.Logic.Function.Conjugate

Cited by

82 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms