English
Let f be an order isomorphism f: α ≃o β and S a LowerSet in α. Then the complement of the image of S under f equals the image under f of the complement of S, viewed as an upper set in β. In symbols: (map f S).compl = UpperSet.map f S.compl.
Русский
Пусть f — изоморфизм порядка f: α ≃o β и S — нижнее множество в α. Тогда комплемент образа S под f равен образу комплемента S под f, рассматриваемому как верхнее множество в β. То есть: (map f S).compl = UpperSet.map f S.compl.
LaTeX
$$$ (\mathrm{map} \, f \, s)^{\mathrm{compl}} = \mathrm{UpperSet.map} \, f \, s^{\mathrm{compl}} $$$
Lean4
@[simp]
theorem compl_map (f : α ≃o β) (s : LowerSet α) : (map f s).compl = UpperSet.map f s.compl :=
SetLike.coe_injective (Set.image_compl_eq f.bijective).symm
