Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-30 00:01 6fc2df65

View on Github →

feat(order/filter/{prod,pi}): add filter.prod_le_prod, filter.pi_le_pi etc (#16468)

Estimated changes

Modified src/data/set/prod.lean

added theorem set.subset_eval_image_pi

Modified src/order/filter/pi.lean

added theorem filter.map_eval_pi

added theorem filter.pi_inj

added theorem filter.pi_le_pi

Modified src/order/filter/prod.lean

added theorem filter.map_fst_prod

added theorem filter.map_snd_prod

added theorem filter.prod_inj

added theorem filter.prod_le_prod

Modified src/topology/inseparable.lean

added theorem inseparable.prod

added theorem inseparable_pi

added theorem inseparable_prod

added theorem specializes.prod

added theorem specializes_pi

added theorem specializes_prod