English
Conjugating closure operators on α and β by a fixed order isomorphism e gives an equivalence ClosureOperator(α) ≃ ClosureOperator(β).
Русский
Сопряжение замыкателей на α и β фиксированным изоморфизмом порядка e задаёт эквивалентность ClosureOperator(α) ≃ ClosureOperator(β).
LaTeX
$$$\\text{equivClosureOperator}(e) : ClosureOperator(\\alpha) \\simeq ClosureOperator(\\beta)$$$
Lean4
/-- Conjugating `ClosureOperators` on `α` and on `β` by a fixed isomorphism
`e : α ≃o β` gives an equivalence `ClosureOperator α ≃ ClosureOperator β`. -/
@[simps apply symm_apply]
def equivClosureOperator {α β} [Preorder α] [Preorder β] (e : α ≃o β) : ClosureOperator α ≃ ClosureOperator β
where
toFun c := c.conjBy e
invFun c := c.conjBy e.symm
left_inv c := Eq.trans (c.conjBy_trans _ _).symm <| Eq.trans (congrArg _ e.self_trans_symm) c.conjBy_refl
right_inv c := Eq.trans (c.conjBy_trans _ _).symm <| Eq.trans (congrArg _ e.symm_trans_self) c.conjBy_refl
