English
Define a continuous map productOfMemOpens : X → Opens(X) → Prop by productOfMemOpens(x)(u) = (x ∈ u). This map assigns to each point the predicate of membership across all open sets.
Русский
Определим отображение productOfMemOpens : X → Opens(X) → Prop по формуле productOfMemOpens(x)(u) = (x ∈ u). Это отображение фиксирует для каждого x предикат принадлежности в каждом открытом множестве.
LaTeX
$$$\text{productOfMemOpens}: C(X, \mathrm{Opens}(X) \to \mathbf{Prop})\;\text{с}\\toFun(x,u) = (x \in u).$$$
Lean4
/-- The continuous map from `X` to the product of copies of the Sierpinski space, (one copy for each
open subset `u` of `X`). The `u` coordinate of `productOfMemOpens x` is given by `x ∈ u`.
-/
def productOfMemOpens : C(X, Opens X → Prop) where
toFun x u := x ∈ u
continuous_toFun := continuous_pi_iff.2 fun u => continuous_Prop.2 u.isOpen
