English
Given a closure operator c on α and an order isomorphism e: α ≃o β, the conjugate e ∘ c ∘ e⁻¹ is a closure operator on β.
Русский
Для замыкателя c на α и изоморфизма порядка e: α ≃o β свертка e ∘ c ∘ e⁻¹ образует замыкатель на β.
LaTeX
$$conjBy(c,e) : ClosureOperator β$$
Lean4
/-- If `c` is a closure operator on `α` and `e` an order-isomorphism
between `α` and `β` then `e ∘ c ∘ e⁻¹` is a closure operator on `β`. -/
@[simps apply]
def conjBy {α β} [Preorder α] [Preorder β] (c : ClosureOperator α) (e : α ≃o β) : ClosureOperator β
where
toFun := e.conj c
IsClosed b := c.IsClosed (e.symm b)
monotone' _ _ h := (map_le_map_iff e).mpr <| c.monotone <| (map_le_map_iff e.symm).mpr h
le_closure' _ := e.symm_apply_le.mp (c.le_closure' _)
idempotent' _ := congrArg e <| Eq.trans (congrArg c (e.symm_apply_apply _)) (c.idempotent' _)
isClosed_iff := Iff.trans c.isClosed_iff e.eq_symm_apply
