Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-28 08:10 2f6a5f59

View on Github →

feat(nat, lattice): preliminaries for Haar measure (#3190) PR 2/5 to put the Haar measure in mathlib. This PR: results about lattices and lattice operations on nat. add some simp lemmas for nat.find (simplifying a proof in sum_four_squares) rename finset.sup_val to finset.sup_def (it was unused). In PR 3 I will add a new declaration finset.sup_val Inf_nat_def and Sup_nat_def renamed to nat.Inf_def and nat.Sup_def, and use set.nonempty in statement (they were unused outside that file)

Estimated changes

added theorem finset.sup_def
deleted theorem finset.sup_val
added theorem nat.find_eq_zero
added theorem nat.find_pos
modified theorem Inf_range
modified theorem Sup_range
added theorem infi_and'
modified theorem infi_apply
added theorem infi_congr
modified theorem infi_congr_Prop
modified theorem infi_prod
modified theorem infi_sigma
modified theorem infi_sum
added theorem supr_and'
modified theorem supr_apply
added theorem supr_congr
modified theorem supr_congr_Prop
modified theorem supr_prod
modified theorem supr_sigma
modified theorem supr_sum
deleted theorem Inf_nat_def
deleted theorem Sup_nat_def
added theorem nat.Inf_def
added theorem nat.Inf_eq_zero
added theorem nat.Inf_mem
added theorem nat.Sup_def
added theorem nat.not_mem_of_lt_Inf