Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-31 09:48 cafeaa35

View on Github →

feat(data/set/lattice): add lemmas about unions over natural numbers (#14393)

  • Add Union/Inter versions of lemmas like supr_ge_eq_supr_nat_add.
  • Make some arguments explicit.

Estimated changes

added theorem antitone.Inter_nat_add
added theorem monotone.Union_nat_add
added theorem antitone.infi_nat_add
modified theorem infi_ge_eq_infi_nat_add
modified theorem supr_ge_eq_supr_nat_add