English
If two sets are order-antitone isomorphic, their maximals and minimals correspond under the induced duality.
Русский
Если два множества антотонически изоморфны, их максимумы и минимумы соответствуют через индуцированную двойственность.
LaTeX
$$$\\forall f:\\, s \\simeq_o t^{\\mathrm{op}},\\; {x \\mid \\operatorname{Maximal}(\\cdot \\in s) x} \\cong_o {x \\mid \\operatorname{Minimal}(\\cdot \\in t) x}$$$
Lean4
/-- If two sets are order isomorphic, their maximals are also order isomorphic. -/
def mapSetOfMaximal (f : s ≃o t) : {x | Maximal (· ∈ s) x} ≃o {x | Maximal (· ∈ t) x}
where
toFun x := ⟨f ⟨x, x.2.1⟩, f.map_maximal_mem x.2⟩
invFun x := ⟨f.symm ⟨x, x.2.1⟩, f.symm.map_maximal_mem x.2⟩
left_inv x := Subtype.ext (congr_arg Subtype.val <| f.left_inv ⟨x, x.2.1⟩ :)
right_inv x := Subtype.ext (congr_arg Subtype.val <| f.right_inv ⟨x, x.2.1⟩ :)
map_rel_iff' := f.map_rel_iff
