Theorems · Theorem · order theory

Function.semiconj_of_isLUB

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

Defined in

Mathlib.Order.SemiconjSup

Cited by

2 results in Mathlib

Foundations

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

Assumes

PartialOrderGroup