Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-18 18:51 4af7699b

View on Github →

feat(order/upper_lower): Maps of upper sets (#17007) An order isomorphism of preorders induces an order isomorphisms of their upper sets.

Estimated changes

modified theorem set.Inter_false
added theorem set.Inter_of_empty
modified theorem set.Union_false
added theorem set.Union_of_empty
added theorem set.image_Inter
added theorem set.image_Inter₂
added theorem order_iso.symm_trans
modified theorem coe_lower_closure
modified theorem coe_upper_closure
added theorem is_lower_set.image
added theorem is_lower_set.preimage
added theorem is_upper_set.image
added theorem is_upper_set.preimage
added theorem lower_closure_image
added theorem lower_set.coe_map
added theorem lower_set.compl_map
added def lower_set.map
added theorem lower_set.map_Iic
added theorem lower_set.map_Iio
added theorem lower_set.map_map
added theorem lower_set.map_refl
added theorem lower_set.mem_map
added theorem lower_set.mem_mk
added theorem lower_set.symm_map
added theorem upper_closure_image
added theorem upper_set.coe_map
added theorem upper_set.compl_map
added def upper_set.map
added theorem upper_set.map_Ici
added theorem upper_set.map_Ioi
added theorem upper_set.map_map
added theorem upper_set.map_refl
added theorem upper_set.mem_map
added theorem upper_set.mem_mk
added theorem upper_set.symm_map