Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-11 09:33 f5170fc5

View on Github →

feat(order/bounded_order): Codisjointness (#14195) Define codisjoint, the dual notion of disjoint. This is already used without a name in is_compl, and will soon be used for Heyting algebras.

Estimated changes

added theorem bot_codisjoint
added theorem codisjoint.comm
added theorem codisjoint.dual
added theorem codisjoint.eq_top
added theorem codisjoint.inf_left
added theorem codisjoint.inf_right
added theorem codisjoint.mono
added theorem codisjoint.mono_left
added theorem codisjoint.mono_right
added theorem codisjoint.ne
added theorem codisjoint.sup_left'
added theorem codisjoint.sup_left
added theorem codisjoint.sup_right'
added theorem codisjoint.sup_right
added theorem codisjoint.symm
added def codisjoint
added theorem codisjoint_assoc
added theorem codisjoint_bot
added theorem codisjoint_iff
added theorem codisjoint_inf_left
added theorem codisjoint_inf_right
added theorem codisjoint_of_dual_iff
added theorem codisjoint_self
added theorem codisjoint_to_dual_iff
added theorem codisjoint_top_left
added theorem codisjoint_top_right
added theorem disjoint.dual
added theorem disjoint_of_dual_iff
added theorem disjoint_to_dual_iff
modified theorem is_compl.of_eq
modified theorem is_compl.sup_eq_top
modified structure is_compl
added theorem symmetric_codisjoint
modified theorem order_embedding.le_map_sup
modified theorem order_embedding.map_inf_le
modified theorem order_iso.map_inf
modified theorem order_iso.map_sup
added theorem codisjoint.map
modified theorem is_compl.map