Commit 2022-11-28 22:38 4449a0ad

View on Github →

feat: port Order.Disjoint (#773) sha 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Disjoint.lean

added theorem Codisjoint.comm

added theorem Codisjoint.dual

added theorem Codisjoint.eq_top

added theorem Codisjoint.eq_top_of_ge

added theorem Codisjoint.eq_top_of_le

added theorem Codisjoint.inf_left

added theorem Codisjoint.inf_right

added theorem Codisjoint.left_le_of_le_inf_left

added theorem Codisjoint.left_le_of_le_inf_right

added theorem Codisjoint.mono

added theorem Codisjoint.mono_left

added theorem Codisjoint.mono_right

added theorem Codisjoint.ne

added theorem Codisjoint.of_codisjoint_sup_of_le'

added theorem Codisjoint.of_codisjoint_sup_of_le

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 theorem Codisjoint.top_le

added def Codisjoint

added theorem Disjoint.comm

added theorem Disjoint.dual

added theorem Disjoint.eq_bot

added theorem Disjoint.eq_bot_of_ge

added theorem Disjoint.eq_bot_of_le

added theorem Disjoint.inf_left'

added theorem Disjoint.inf_left

added theorem Disjoint.inf_right'

added theorem Disjoint.inf_right

added theorem Disjoint.le_bot

added theorem Disjoint.le_of_codisjoint

added theorem Disjoint.left_le_of_le_sup_left

added theorem Disjoint.left_le_of_le_sup_right

added theorem Disjoint.mono

added theorem Disjoint.mono_left

added theorem Disjoint.mono_right

added theorem Disjoint.ne

added theorem Disjoint.of_disjoint_inf_of_le'

added theorem Disjoint.of_disjoint_inf_of_le

added theorem Disjoint.sup_left

added theorem Disjoint.sup_right

added theorem Disjoint.symm

added def Disjoint

added theorem IsCompl.disjoint_left_iff

added theorem IsCompl.disjoint_right_iff

added theorem IsCompl.dual

added theorem IsCompl.inf_eq_bot

added theorem IsCompl.inf_left_eq_bot_iff

added theorem IsCompl.inf_left_le_of_le_sup_right

added theorem IsCompl.inf_right_eq_bot_iff

added theorem IsCompl.inf_sup

added theorem IsCompl.le_left_iff

added theorem IsCompl.le_right_iff

added theorem IsCompl.le_sup_right_iff_inf_left_le

added theorem IsCompl.left_le_iff

added theorem IsCompl.left_unique

added theorem IsCompl.ofDual

added theorem IsCompl.of_eq

added theorem IsCompl.of_le

added theorem IsCompl.right_le_iff

added theorem IsCompl.right_unique

added theorem IsCompl.sup_eq_top

added theorem IsCompl.sup_inf

added structure IsCompl

added theorem bot_codisjoint

added theorem codisjoint_assoc

added theorem codisjoint_bot

added theorem codisjoint_iff

added theorem codisjoint_iff_le_sup

added theorem codisjoint_inf_left

added theorem codisjoint_inf_right

added theorem codisjoint_left_comm

added theorem codisjoint_ofDual_iff

added theorem codisjoint_right_comm

added theorem codisjoint_self

added theorem codisjoint_toDual_iff

added theorem codisjoint_top_left

added theorem codisjoint_top_right

added theorem disjoint_assoc

added theorem disjoint_bot_left

added theorem disjoint_bot_right

added theorem disjoint_iff

added theorem disjoint_iff_inf_le

added theorem disjoint_left_comm

added theorem disjoint_ofDual_iff

added theorem disjoint_right_comm

added theorem disjoint_self

added theorem disjoint_sup_left

added theorem disjoint_sup_right

added theorem disjoint_toDual_iff

added theorem disjoint_top

added theorem eq_bot_of_isCompl_top

added theorem eq_bot_of_top_isCompl

added theorem eq_top_of_bot_isCompl

added theorem eq_top_of_isCompl_bot

added theorem isCompl_bot_top

added theorem isCompl_iff

added theorem isCompl_ofDual_iff

added theorem isCompl_toDual_iff

added theorem isCompl_top_bot

added theorem symmetric_codisjoint

added theorem symmetric_disjoint

added theorem top_disjoint