semiconj_iff_comp_eq — Mathlib

English

A function f semiconjugates ga to gb if and only if f ∘ ga = gb ∘ f.

Русский

Функция f полусопряжена с ga к gb тогда, когда f ∘ ga = gb ∘ f.

LaTeX

$$$ \forall {\alpha} {\beta} {\gamma} {f : \alpha \to \beta} {ga : \alpha \to \alpha} {gb : \beta \to \beta},\; (\operatorname{Semiconj} f ga gb) \iff (f \circ ga = gb \circ f)$$$

Lean4

/-- Definition of `Function.Semiconj` in terms of functional equality. -/
theorem _root_.Function.semiconj_iff_comp_eq : Semiconj f ga gb ↔ f ∘ ga = gb ∘ f :=
  funext_iff.symm

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