Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-10 15:39 3cc7a32b

View on Github →

feat(order/complete_lattice): add a constructor from partial_order and Inf (#2359) Also use ∃! in data/setoid.

Estimated changes

deleted theorem setoid.Inf_le
modified theorem setoid.classes_eqv_classes
modified theorem setoid.eq_of_mem_eqv_class
modified theorem setoid.eqv_class_mem
modified theorem setoid.eqv_classes_disjoint
deleted theorem setoid.le_Inf
modified def setoid.mk_classes
deleted theorem con.Inf_le
modified theorem con.con_gen_of_con
deleted theorem con.le_Inf
modified theorem lower_bounds_insert
modified theorem lower_bounds_singleton
modified theorem upper_bounds_insert
modified theorem upper_bounds_singleton