Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-01 15:09 0a0a60cc

View on Github →

feat(data/set/finite,order/*): generalize some lemmas from sets to (co)frames (#14394)

generalize set.Union_inter_of_monotone to an order.frame;
add dual versions, both for (co)frames and sets;
same for set.Union_Inter_of_monotone.

Estimated changes

Modified src/data/set/finite.lean

added theorem infi_supr_of_antitone

added theorem infi_supr_of_monotone

added theorem set.Inter_Union_of_antitone

added theorem set.Inter_Union_of_monotone

added theorem set.Union_Inter_of_antitone

modified theorem set.Union_Inter_of_monotone

added theorem set.finite.infi_bsupr_of_antitone

added theorem set.finite.infi_bsupr_of_monotone

added theorem set.finite.supr_binfi_of_antitone

added theorem set.finite.supr_binfi_of_monotone

added theorem supr_infi_of_antitone

added theorem supr_infi_of_monotone

Modified src/data/set/lattice.lean

added theorem set.Inter_union_of_antitone

added theorem set.Inter_union_of_monotone

added theorem set.Union_inter_of_antitone

modified theorem set.Union_inter_of_monotone

Modified src/order/complete_boolean_algebra.lean

added theorem infi_sup_of_antitone

added theorem infi_sup_of_monotone

added theorem supr_inf_of_antitone

added theorem supr_inf_of_monotone

Modified src/order/complete_lattice.lean

added theorem infi_sup_infi_le

added theorem le_supr_inf_supr

added theorem supr_infi_le_infi_supr