Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-17 23:41 5b4425ae

View on Github →

feat(order/lattice): Congruence lemmas for ⊔ and ⊓ (#15439) a ⊔ b = a ⊔ c if b ≤ a ⊔ c and c ≤ a ⊔ b, and similar.

Lemma renames

sup_eq_sup_of_le_le → sup_congr_right
inf_eq_inf_of_le_le → inf_congr_right
set.union_eq_union_of_subset_of_subset → set.union_congr_right
set.inter_eq_inter_of_subset_of_subset → set.inter_congr_right

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.inter_congr_left

added theorem finset.inter_congr_right

added theorem finset.inter_eq_inter_iff_left

added theorem finset.inter_eq_inter_iff_right

added theorem finset.union_congr_left

added theorem finset.union_congr_right

added theorem finset.union_eq_union_iff_left

added theorem finset.union_eq_union_iff_right

Modified src/data/set/basic.lean

added theorem set.inter_congr_left

added theorem set.inter_congr_right

added theorem set.inter_eq_inter_iff_left

added theorem set.inter_eq_inter_iff_right

deleted theorem set.inter_eq_inter_iff_subset_subset

deleted theorem set.inter_eq_inter_of_subset_of_subset

added theorem set.union_congr_left

added theorem set.union_congr_right

added theorem set.union_eq_union_iff_left

added theorem set.union_eq_union_iff_right

deleted theorem set.union_eq_union_iff_subset_subset

deleted theorem set.union_eq_union_of_subset_of_subset

Modified src/order/boolean_algebra.lean

added theorem sup_sdiff_eq_sup

Modified src/order/lattice.lean

added theorem inf_congr_left

added theorem inf_congr_right

deleted theorem inf_eq_inf_iff_le_le

added theorem inf_eq_inf_iff_left

added theorem inf_eq_inf_iff_right

deleted theorem inf_eq_inf_of_le_of_le

added theorem sup_congr_left

added theorem sup_congr_right

deleted theorem sup_eq_sup_iff_le_le

added theorem sup_eq_sup_iff_left

added theorem sup_eq_sup_iff_right

deleted theorem sup_eq_sup_of_le_of_le