doc(Order/Filter/*): outdated documents (leanprover-community#33211)

`f ×ˢ g` is not an notation of `Filter.prod` anymore, but [a notation class](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Filter/Defs.html#Filter.instSProd).
Also, some definitions were moved to `Mathlib.Order.Filter.Defs`.

Co-authored-by: Komyyy <pol_tta@outlook.jp>

Author: Komyyy

Mathlib/Order/Filter/Curry.lean

@@ -27,9 +27,11 @@ Another way to think about the curried versus the product filter is that tending
 the product filter is a version of uniform convergence (see `tendsto_prod_filter_iff`) whereas
 tending to some limit on a curried filter is just iterated limits (see `Filter.Tendsto.curry`).
 
-In the "generalized set" intuition, `Filter.prod` and `Filter.curry` correspond to two ways of
-describing the product of two sets, namely `s ×ˢ t = fst ⁻¹' s ∩ snd ⁻¹' t` and
-`s ×ˢ t = ⋃ x ∈ s, (x, ·) '' t`.
+In the "generalized set" intuition, a product filter and `Filter.curry` correspond to two ways
+of describing the product of two sets:
+
+* `f ×ˢ g = comap fst f ⊓ comap snd g` corresponds to `s ×ˢ t = fst ⁻¹' s ∩ snd ⁻¹' t`
+* `f.curry g = bind f (fun x ↦ map (x, ·) g)` corresponds to `s ×ˢ t = ⋃ x ∈ s, (x, ·) '' t`
 
 ## Main definitions
 

Mathlib/Order/Filter/Pi.lean

@@ -12,12 +12,12 @@ public import Mathlib.Order.Filter.Bases.Finite
 /-!
 # (Co)product of a family of filters
 
-In this file we define two filters on `Π i, α i` and prove some basic properties of these filters.
+In this file we prove some basic properties of two filters on `Π i, α i`.
 
 * `Filter.pi (f : Π i, Filter (α i))` to be the maximal filter on `Π i, α i` such that
   `∀ i, Filter.Tendsto (Function.eval i) (Filter.pi f) (f i)`. It is defined as
-  `Π i, Filter.comap (Function.eval i) (f i)`. This is a generalization of `Filter.prod` to indexed
-  products.
+  `Π i, Filter.comap (Function.eval i) (f i)`. This is a generalization of binary products to
+  indexed products.
 
 * `Filter.coprodᵢ (f : Π i, Filter (α i))`: a generalization of `Filter.coprod`; it is the supremum
   of `comap (eval i) (f i)`.

Mathlib/Order/Filter/Prod.lean

@@ -10,7 +10,7 @@ public import Mathlib.Order.Filter.Tendsto
 /-!
 # Product and coproduct filters
 
-In this file we define `Filter.prod f g` (notation: `f ×ˢ g`) and `Filter.coprod f g`. The product
+In this file we prove some basic properties of `f ×ˢ g` and `Filter.coprod f g`. The product
 of two filters is the largest filter `l` such that `Filter.Tendsto Prod.fst l f` and
 `Filter.Tendsto Prod.snd l g`.
 
@@ -30,10 +30,6 @@ s ∈ G  ↔  ∀ i:ℕ, ∃ n, [n..∞] × {i} ⊆ s
 Now `⋃ i, [i..∞] × {i}` is in `G` but not in `F`.
 As product filter we want to have `F` as result.
 
-## Notation
-
-* `f ×ˢ g` : `Filter.prod f g`, localized in `Filter`.
-
 -/
 
 @[expose] public section