mathlib3
d24faea6 - chore(data/real/basic): drop some lemmas (#8523)

Commit
4 years ago
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_lattice`s instead. Also drop unneeded assumptions in `real.lt_Inf_add_pos` and `real.add_neg_lt_Sup`.
Author
Parents
Loading