orderIso_comp — Mathlib

English

If there is a right adjoint for f, it behaves well under an order isomorphism e: β ≃o γ.

Русский

Если для f существует правая сопряжённость, она сохраняется под перестановкой порядка e: β ≃o γ.

LaTeX

$$$\\text{IsOrderRightAdjoint } f g \\to ∀ e : β \\simeq_o γ, \\ IsOrderRightAdjoint (e \\circ f) (g \\circ e^{-1}).$$$

Lean4

theorem orderIso_comp [Preorder α] [Preorder β] [Preorder γ] {f : α → β} {g : β → α} (h : IsOrderRightAdjoint f g)
    (e : β ≃o γ) : IsOrderRightAdjoint (e ∘ f) (g ∘ e.symm) := fun y => by simpa [e.le_symm_apply] using h (e.symm y)

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