Theorems · Theorem · order theory

Function.sSup_div_semiconj

∀ {α : Type u_1} {G : Type u_4} [inst : CompleteLattice α] [inst_1 : Group G] (f₁ f₂ : G →* α ≃o α) (g : G),
  Function.Semiconj (fun x => ⨆ g', (f₁ g')⁻¹ ((f₂ g') x)) ⇑(f₂ g) ⇑(f₁ g)

Consider two actions f₁ f₂ : G → α → α of a group on a complete lattice by order isomorphisms. Then the map x ↦ ⨆ g : G, (f₁ g)⁻¹ (f₂ g x) semiconjugates each f₁ g' to f₂ g'. This is a version of Proposition 5.4 from [Étienne Ghys, Groupes d'homéomorphismes du cercle et cohomologie bornée][ghys87:groupes].

Defined in

Mathlib.Order.SemiconjSup

Cited by

0 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Quot.sound

Assumes

CompleteLatticeGroup