English
Let f1, f2 be monoid homomorphisms defining order automorphisms; if for every x the set { (f1 g')^{-1}(f2 g' x) | g' ∈ G } has h x as a least upper bound, then h semiconjugates f2 g with f1 g for every g.
Русский
Пусть f1, f2 — моноидные гомоморфизмы, задающие порядка-автоморфизм; если для каждого x множество { (f1 g')^{-1}(f2 g' x) } имеет наибольшую нижнюю грань h x, тогда для каждого g имеем semiconjugacy: h ∘ (f2 g) = (f1 g) ∘ h.
LaTeX
$$$\forall g:\ G,\ h\circ (f_2 g) = (f_1 g) \circ h$ при условии $\forall x, IsLUB(\{ (f_1 g')^{-1}(f_2 g' x) \mid g'\in G\}) (h x)$$$
Lean4
theorem semiconj_of_isLUB [PartialOrder α] [Group G] (f₁ f₂ : G →* α ≃o α) {h : α → α}
(H : ∀ x, IsLUB (range fun g' => (f₁ g')⁻¹ (f₂ g' x)) (h x)) (g : G) : Function.Semiconj h (f₂ g) (f₁ g) :=
by
refine fun y => (H _).unique ?_
have := (f₁ g).leftOrdContinuous (H y)
rw [← range_comp, ← (Equiv.mulRight g).surjective.range_comp _] at this
simpa [comp_def] using this
