Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-28 14:39 5c221a31

View on Github →

feat(order/conditionally_complete_lattic): nat is a conditionally complete linear order with bottom

Estimated changes

Modified algebra/ordered_ring.lean

Modified data/equiv/list.lean

Modified order/conditionally_complete_lattice.lean

added theorem lattice.Inf_nat_def

added theorem lattice.Sup_nat_def