Commit 2023-07-29 10:37 adddab87

View on Github →

feat(Data/Set/Lattice, Order/Filter/Basic): more lemmas about kernImage and filter analog (#5744) This was originally discussed on Zulip, and Junyan made most of the work in this message. I just changed some proofs to use a bit more Galois connections. This is a bit of a gadget but it does simplify the proof of comap_iSup, and it will also be convenient to define the space of functions with support a compact subset of a fixed set. See this message for more details.

Estimated changes

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.compl_range_subset_kernImage

added theorem Set.kernImage_compl

added theorem Set.kernImage_empty

added theorem Set.kernImage_eq_compl

added theorem Set.kernImage_mono

added theorem Set.kernImage_preimage_eq_iff

added theorem Set.kernImage_preimage_union

added theorem Set.kernImage_union_preimage

added theorem Set.subset_kernImage_iff

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.comap_le_iff_le_kernMap

added theorem Filter.compl_mem_kernMap

added theorem Filter.gc_comap_kernMap

added def Filter.kernMap

added theorem Filter.kernMap_principal

added theorem Filter.mem_comap''

added theorem Filter.mem_kernMap

added theorem Filter.mem_kernMap_iff_compl

Modified Mathlib/Order/GaloisConnection.lean