English
Dual statement to the previous: minimal elements correspond to maximal under a duality-induced iso.
Русский
Двойственное утверждение: минимальные элементы соответствуют максимальным через изоморфизм, индуцируемый двойственностью.
LaTeX
$$$\\forall f:\\, s \\simeq_o t^{\\mathrm{op}},\\; {x \\mid \\operatorname{Minimal}(\\cdot \\in s) x} \\cong_o {x \\mid \\operatorname{Maximal}(\\cdot \\in t) x}$$$
Lean4
/-- If two sets are antitonically order isomorphic, their minimals/maximals are too. -/
def setOfMinimalIsoSetOfMaximal (f : s ≃o tᵒᵈ) : {x | Minimal (· ∈ s) x} ≃o {x | Maximal (· ∈ t) (ofDual x)}
where
toFun x := ⟨(f ⟨x.1, x.2.1⟩).1, ((show s ≃o ofDual ⁻¹' t from f).mapSetOfMinimal x).2⟩
invFun x := ⟨(f.symm ⟨x.1, x.2.1⟩).1, ((show ofDual ⁻¹' t ≃o s from f.symm).mapSetOfMinimal x).2⟩
__ := (show s ≃o ofDual ⁻¹' t from f).mapSetOfMinimal
