comp_orderIso — Mathlib

English

If h is right adjoint for f and e is an order isomorphism, then the composed adjoint holds for f∘e and e.symm∘g.

Русский

Если h — правая сопряжённость к f и e — перестановка порядка, то сопряжённость сохраняется для f∘e и e.symm∘g.

LaTeX

$$$\\forall y, IsLUB( e^{-1}'{x | f x ≤ y}, e^{-1}(g y)).$$$

Lean4

theorem comp_orderIso [Preorder α] [Preorder β] [Preorder γ] {f : α → β} {g : β → α} (h : IsOrderRightAdjoint f g)
    (e : γ ≃o α) : IsOrderRightAdjoint (f ∘ e) (e.symm ∘ g) :=
  by
  intro y
  change IsLUB (e ⁻¹' {x | f x ≤ y}) (e.symm (g y))
  rw [e.isLUB_preimage, e.apply_symm_apply]
  exact h y

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