Commit 2022-07-01 18:31 ff5e97ad

View on Github →

feat(order/lattice, data/set): some helper lemmas (#14789) This PR provides lemmas describing when s ∪ a = t ∪ a, in both necessary and iff forms, as well as intersection and lattice versions.

Estimated changes

Modified src/data/set/basic.lean

added theorem set.inter_eq_inter_iff_subset_subset

added theorem set.inter_eq_inter_of_subset_of_subset

added theorem set.union_eq_union_iff_subset_subset

added theorem set.union_eq_union_of_subset_of_subset

Modified src/order/lattice.lean

added theorem inf_eq_inf_iff_le_le

added theorem inf_eq_inf_of_le_of_le

added theorem sup_eq_sup_iff_le_le

added theorem sup_eq_sup_of_le_of_le