Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-28 17:40 b1818660

View on Github →

feat(data/set): more lemmas (#6474)

Estimated changes

Modified src/data/set/finite.lean

added theorem set.finite_option

added theorem set.subsingleton.finite

Modified src/data/set/lattice.lean

modified theorem set.Inter_const

added theorem set.Inter_option

modified theorem set.Union_const

added theorem set.Union_option

added theorem set.disjoint_Union_left

added theorem set.disjoint_Union_right

Modified src/order/complete_boolean_algebra.lean

added theorem disjoint_supr_iff

added theorem inf_supr_eq

added theorem infi_sup_eq

added theorem sup_infi_eq

added theorem supr_disjoint_iff

added theorem supr_inf_eq

Modified src/order/complete_lattice.lean

added theorem infi_option

added theorem supr_option