English
Another dual: maximal elements under an anti-isomorphism correspond to minimal elements in the opposite.
Русский
Еще одно двойственное утверждение: максимальные элементы при антиизоморфизме соответствуют минимальным элементам в противоложе.
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 antitonically order isomorphic, their maximals/minimals are too. -/
def setOfMaximalIsoSetOfMinimal (f : s ≃o tᵒᵈ) : {x | Maximal (· ∈ s) x} ≃o {x | Minimal (· ∈ t) (ofDual x)}
where
toFun x := ⟨(f ⟨x.1, x.2.1⟩).1, ((show s ≃o ofDual ⁻¹' t from f).mapSetOfMaximal x).2⟩
invFun x := ⟨(f.symm ⟨x.1, x.2.1⟩).1, ((show ofDual ⁻¹' t ≃o s from f.symm).mapSetOfMaximal x).2⟩
__ := (show s ≃o ofDual ⁻¹' t from f).mapSetOfMaximal
