Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-07 19:36 0f240304

View on Github →

refactor(src/data/finset): supr/infi as a directed supr/infi of finite inf/sup

Estimated changes

Modified src/data/finset.lean

added theorem finset.inf_congr

added theorem finset.sup_congr

added theorem lattice.infi_eq_infi_finset

added theorem lattice.supr_eq_supr_finset

added theorem set.Inter_eq_Inter_finset

added theorem set.Union_eq_Union_finset

Modified src/data/set/lattice.lean

added theorem set.monotone_inter

added theorem set.monotone_set_of

added theorem set.monotone_union

Modified src/order/filter.lean

deleted theorem filter.Inf_sets_eq_finite

deleted theorem filter.binfi_sup_eq

modified theorem filter.infi_sets_eq'

added theorem filter.infi_sets_eq_finite

modified theorem filter.infi_sup_eq

modified theorem filter.supr_join

deleted theorem lattice.Inf_eq_finite_sets

deleted theorem lattice.inf_left_comm

deleted theorem lattice.infi_empty_finset

deleted theorem lattice.infi_insert_finset

deleted theorem set.monotone_inter

deleted theorem set.monotone_set_of

Modified src/order/lattice.lean

added theorem lattice.directed_of_inf

added theorem lattice.directed_of_sup

added theorem lattice.inf_left_comm

added theorem lattice.sup_left_comm