English
Under a suitable order-preserving structure, the minimal elements correspond under isomorphism.
Русский
При допустимой сохранности порядка минимальные элементы сопоставляются через изоморфизм.
LaTeX
$$$\\forall f:\\, s \\cong_o t,\\; (f.map_minimal_mem x) \\Rightarrow (\\text{Minimal}(\\cdot \\in t) (f x))$$$
Lean4
/-- If two sets are order isomorphic, their minimals are also order isomorphic. -/
def mapSetOfMinimal (f : s ≃o t) : {x | Minimal (· ∈ s) x} ≃o {x | Minimal (· ∈ t) x}
where
toFun x := ⟨f ⟨x, x.2.1⟩, f.map_minimal_mem x.2⟩
invFun x := ⟨f.symm ⟨x, x.2.1⟩, f.symm.map_minimal_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
