Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-11 18:26 ce09c18f

View on Github →

add Galois connection, also add a couple of order theoretic results

Estimated changes

added def preorder_dual
added theorem eq_of_is_glb_of_is_glb
added theorem eq_of_is_lub_of_is_lub
added theorem is_glb_Inf
added theorem is_glb_empty
added theorem is_glb_iff_Inf_eq
added theorem is_glb_iff_inf_eq
added theorem is_glb_iff_infi_eq
added theorem is_glb_infi
added theorem is_glb_insert_inf
added theorem is_glb_singleton
added theorem is_glb_union_inf
added theorem is_lub_Sup
added theorem is_lub_empty
added theorem is_lub_iff_Sup_eq
added theorem is_lub_iff_sup_eq
added theorem is_lub_iff_supr_eq
added theorem is_lub_insert_sup
added theorem is_lub_singleton
added theorem is_lub_supr
added theorem is_lub_union_sup
added theorem mem_lower_bounds_image
added theorem mem_upper_bounds_image
added theorem galois_connection.l_le
added theorem galois_connection.le_u