Commit 2021-08-13 21:43 94e4667b

feat(order/filter): change definition of inf (#8657) The current definition of filter.inf came directly from the Galois insertion: u ∈ f ⊓ g if it contains s ∩ t for some s ∈ f and t ∈ g, but the new one is tidier: u ∈ f ⊓ g if u = s ∩ t for some s ∈ f and t ∈ g. This gives a stronger assertion to work with when assuming a set belongs to a filter inf. On the other hand it makes it harder to prove such a statement so we keep the old version as a lemma filter.mem_inf_of_inter : ∀ {f g : filter α} {s t u : set α}, s ∈ f → t ∈ g → s ∩ t ⊆ u → u ∈ f ⊓ g. Also renames lots of lemmas to remove the word "sets" that was a remnant of the very early days. In passing I also changed the simp lemma filter.mem_map from t ∈ map m f ↔ {x | m x ∈ t} ∈ f to t ∈ map m f ↔ m ⁻¹' t ∈ f which seemed more normal form to me. But this led to a lot of breakage, so I also kept the old version as mem_map'.