English
A finite product of discrete spaces is discrete. In particular, if each A_i is equipped with the discrete topology and ι is finite, then the product ∏_{i∈ι} A_i carries the discrete topology.
Русский
Конечное произведение дискретных пространств дискретно. Пусть каждое A_i имеет дискретную топологию, и индексировка ι конечна; тогда произведение ∏_{i∈ι} A_i также дискретно.
LaTeX
$$$\\text{Finite } \\iota \\;\\Rightarrow\\; \\operatorname{DiscreteTopology}\\left(\\prod_{i:\\iota} A_i\\right)$.$$
Lean4
/-- Suppose `A i` is a family of topological spaces indexed by `i : ι`, and `X` is a type
endowed with a family of maps `f i : X → A i` for every `i : ι`, hence inducing a
map `g : X → Π i, A i`. This lemma shows that infimum of the topologies on `X` induced by
the `f i` as `i : ι` varies is simply the topology on `X` induced by `g : X → Π i, A i`
where `Π i, A i` is endowed with the usual product topology. -/
theorem inducing_iInf_to_pi {X : Type*} (f : ∀ i, X → A i) :
@IsInducing X (∀ i, A i) (⨅ i, induced (f i) inferInstance) _ fun x i => f i x :=
letI := ⨅ i, induced (f i) inferInstance;
⟨(induced_to_pi _).symm⟩
