Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-13 04:31 a2437102

View on Github →

feat(data/ordinal): well ordering theorem Note to self: this proof seems more cumbersome than it should be. I will see if the proof is easier if we bypass Zorn's lemma.

Estimated changes

added theorem psigma.mk.inj_iff
deleted theorem psigma.mk_eq_mk_iff
added theorem sigma.exists
added theorem sigma.forall
added theorem sigma.mk.inj_iff
deleted theorem sigma.mk_eq_mk_iff
added theorem subtype.exists
added theorem subtype.forall
added theorem sum.exists
added theorem sum.forall
added theorem sum.inl.inj_iff
added theorem sum.inr.inj_iff
added inductive sum.lex
added theorem sum.lex_acc_inl
added theorem sum.lex_acc_inr
added theorem sum.lex_inl_inl
added theorem sum.lex_inr_inl
added theorem sum.lex_inr_inr
added theorem sum.lex_wf
added def sum.swap
added theorem sum.swap_left_inverse
added theorem sum.swap_right_inverse
added theorem sum.swap_swap
added theorem sum.swap_swap_eq
deleted theorem eq_iff_le_and_le
deleted theorem set_of_subset_set_of
deleted theorem sigma.exists
deleted theorem sigma.forall
deleted theorem sigma.mk.inj_iff
deleted theorem subtype.exists
deleted theorem subtype.forall