instAlexandrovDiscreteOfFinite — Mathlib

English

Let ι be a finite index set and X_i be Alexandrov-discrete topological spaces for all i in ι. Then the product ∏_{i∈ι} X_i is Alexandrov-discrete.

Русский

Пусть ι — конечное множество индексирования, и для каждого i∈ι пространство X_i имеет Александрову дискретную топологию. Тогда произведение ∏_{i∈ι} X_i тоже AlexandrovDiscrete.

LaTeX

$$$Finite(ι) \land (\forall i, AlexandrovDiscrete(X_i)) \to AlexandrovDiscrete\left(\prod_{i\in ι} X_i\right)$$$

Lean4

instance instAlexandrovDiscreteOfFinite {ι : Type*} [Finite ι] {X : ι → Type*} [Π i, TopologicalSpace (X i)]
    [∀ i, AlexandrovDiscrete (X i)] : AlexandrovDiscrete (Π i, X i) := by
  simp_rw [alexandrovDiscrete_iff_nhds, nhds_pi, ← principal_nhdsKer_singleton, pi_principal, nhdsKer_singleton_pi,
    forall_true_iff]

Похожие утверждения