Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-04 19:46 d24faea6

View on Github →

chore(data/real/basic): drop some lemmas (#8523) Drop real.Sup_le, real.lt_Sup, real.le_Sup, real.Sup_le_ub, real.le_Inf, real.Inf_lt, real.Inf_le, real.lb_le_Inf. Use lemmas about conditionally_complete_lattices instead. Also drop unneeded assumptions in real.lt_Inf_add_pos and real.add_neg_lt_Sup.

Estimated changes

added theorem set.inv_empty
added theorem set.inv_univ
added theorem set.nonempty.inv
added theorem set.nonempty_inv
modified theorem real.Inf_def
deleted theorem real.Inf_le
deleted theorem real.Inf_lt
deleted theorem real.Sup_le
deleted theorem real.Sup_le_ub
modified theorem real.add_neg_lt_Sup
deleted theorem real.lb_le_Inf
deleted theorem real.le_Inf
deleted theorem real.le_Sup
modified theorem real.lt_Inf_add_pos
deleted theorem real.lt_Sup