Commit 2020-10-31 13:30 e14c3782

refactor(order/filter): move some proofs to bases (#3478) Move some proofs to order/filter/bases and add filter.has_basis versions. Non-bc API changes:

• filter.inf_ne_bot_iff; change ∀ {U V}, U ∈ f → V ∈ g → ... to ∀ ⦃U⦄, U ∈ f → ∀ ⦃V⦄, V ∈ g → ... so that simp lemmas about ∀ U ∈ f can further simplify the result;
• filter.inf_eq_bot_iff: similarly, change ∃ U V, ... to ∃ (U ∈ f) (V ∈ g), ...
• cluster_pt_iff: similarly, change ∀ {U V : set α}, U ∈ 𝓝 x → V ∈ F → ... to ∀ ⦃U : set α⦄ (hU : U ∈ 𝓝 x) ⦃V⦄ (hV : V ∈ F), ...