Commit 2022-12-07 07:48 7967fa9a

View on Github →

feat port: Data.Sum.Order (#880) Mathlib SHA f1a2caaf51ef593799107fe9a8d5e411599f3996 The main difficulty here was having to add a bunch of explicit types where the type was OrderDual when there where funny defeq tricks in Mathlib3.

Estimated changes

added def OrderIso.sumComm
added theorem OrderIso.sumComm_symm
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.inl_strictMono
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_strictMono
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.toLex_le_toLex
added theorem Sum.Lex.toLex_lt_toLex
added theorem Sum.Lex.toLex_mono
added theorem Sum.LiftRel.refl
added theorem Sum.LiftRel.trans
added theorem Sum.denselyOrdered_iff
added theorem Sum.inl_le_inl_iff
added theorem Sum.inl_lt_inl_iff
added theorem Sum.inl_mono
added theorem Sum.inl_strictMono
added theorem Sum.inr_le_inr_iff
added theorem Sum.inr_lt_inr_iff
added theorem Sum.inr_mono
added theorem Sum.inr_strictMono
added theorem Sum.le_def
added theorem Sum.lt_def
added theorem Sum.noMaxOrder_iff
added theorem Sum.noMinOrder_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