Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-20 21:38 d869256e

View on Github →

refactor(data/nat/lattice): move code, add lemmas (#8708)

  • move nat.conditionally_complete_linear_order_with_bot and enat.complete_linear_order to a new file data.nat.lattice;
  • add a few lemmas (nat.supr_lt_succ etc), move set.bUnion_lt_succ to the same file;
  • use galois_insertion.lift_complete_lattice to define enat.complete_linear_order.

Estimated changes

added theorem nat.Inf_def
added theorem nat.Inf_eq_zero
added theorem nat.Inf_mem
added theorem nat.Sup_def
added theorem nat.infi_lt_succ'
added theorem nat.infi_lt_succ
added theorem nat.not_mem_of_lt_Inf
added theorem nat.supr_lt_succ'
added theorem nat.supr_lt_succ
added theorem set.bInter_lt_succ'
added theorem set.bInter_lt_succ
added theorem set.bUnion_lt_succ'
added theorem set.bUnion_lt_succ
deleted theorem set.bInter_lt_succ
deleted theorem set.bUnion_lt_succ
deleted theorem nat.Inf_def
deleted theorem nat.Inf_eq_zero
deleted theorem nat.Inf_mem
deleted theorem nat.Sup_def
deleted theorem nat.nonempty_of_pos_Inf
deleted theorem nat.not_mem_of_lt_Inf