Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-08 07:22 07f9b8e1

View on Github →

feat(data/sum/order): Linear and disjoint sums of orders (#11157) This defines the disjoint sum of two orders on α ⊕ β and the linear (aka lexicographic) sum of two orders on α ⊕ₗ β (a type synonym of α ⊕ β) in a new file data.sum.order.

Estimated changes

modified def equiv.sum_assoc
deleted theorem equiv.sum_assoc_apply_in1
deleted theorem equiv.sum_assoc_apply_in2
deleted theorem equiv.sum_assoc_apply_in3
modified def equiv.sum_comm
added theorem sum.lift_rel.mono
added theorem sum.lift_rel.mono_left
added inductive sum.lift_rel
added theorem sum.lift_rel_inl_inl
added theorem sum.lift_rel_inr_inr
added theorem sum.lift_rel_swap_iff
added theorem sum.inl_le_inl_iff
added theorem sum.inl_lt_inl_iff
added theorem sum.inl_mono
added theorem sum.inl_strict_mono
added def sum.inlₗ
added theorem sum.inr_le_inr_iff
added theorem sum.inr_lt_inr_iff
added theorem sum.inr_mono
added theorem sum.inr_strict_mono
added def sum.inrₗ
added theorem sum.le_def
added theorem sum.lex.inl_bot
added theorem sum.lex.inl_le_inl_iff
added theorem sum.lex.inl_le_inr
added theorem sum.lex.inl_lt_inl_iff
added theorem sum.lex.inl_lt_inr
added theorem sum.lex.inl_mono
added theorem sum.lex.inr_le_inr_iff
added theorem sum.lex.inr_lt_inr_iff
added theorem sum.lex.inr_mono
added theorem sum.lex.inr_top
added theorem sum.lex.le_def
added theorem sum.lex.lt_def
added theorem sum.lex.not_inr_le_inl
added theorem sum.lex.not_inr_lt_inl
added theorem sum.lex.to_lex_mono
added theorem sum.lift_rel.refl
added theorem sum.lift_rel.trans
added theorem sum.lt_def
added theorem sum.no_bot_order_iff
added theorem sum.no_top_order_iff
added theorem sum.not_inl_le_inr
added theorem sum.not_inl_lt_inr
added theorem sum.not_inr_le_inl
added theorem sum.not_inr_lt_inl
added theorem sum.swap_le_swap_iff
added theorem sum.swap_lt_swap_iff
added theorem or.imp3
modified def of_lex
modified def to_lex
added theorem antisymm_of