Commit 2020-12-07 03:33 b2427d53

View on Github →

feat(order/filter/ultrafilter): Restriction of ultrafilters along large embeddings (#5195) This PR adds the fact that the comap of an ultrafilter along a "large" embedding (meaning the image is large w.r.t. the ultrafilter) is again an ultrafilter.

Estimated changes

Modified src/data/set/basic.lean

added theorem set.range_diff_image

added theorem set.range_diff_image_subset

Modified src/order/filter/basic.lean

added theorem filter.image_mem_map_iff

added theorem filter.mem_comap_iff

Modified src/order/filter/ultrafilter.lean

added def filter.ultrafilter.comap