English
Upper sets are order-isomorphic to lower sets via complementation, with the complement map providing the isomorphism in both directions.
Русский
верхние множества пространств упорядочены аналогично нижним множествам через комплементацию; отображение комплемента задает изоморфизм.
LaTeX
$$$ \text{UpperSet}(\alpha) \cong \text{LowerSet}(\alpha) \quad \text{via } s \mapsto s^{\mathrm{c}} , \ t \mapsto t^{\mathrm{c}} $$$
Lean4
/-- Upper sets are order-isomorphic to lower sets under complementation. -/
@[simps]
def upperSetIsoLowerSet : UpperSet α ≃o LowerSet α
where
toFun := UpperSet.compl
invFun := LowerSet.compl
left_inv := UpperSet.compl_compl
right_inv := LowerSet.compl_compl
map_rel_iff' := UpperSet.compl_le_compl
