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