metrizableSpace_pi — Mathlib

English

If each A_i is metrizable, then the Pi-space ∀ i, A_i is metrizable.

Русский

Если каждый A_i метризуем, то пространство Π_i A_i метризуемо.

LaTeX

$$$[\forall i, \text{MetrizableSpace } (A_i)] \Rightarrow [\text{MetrizableSpace } (\forall i, A_i)]$$$

Lean4

instance metrizableSpace_pi [∀ i, MetrizableSpace (A i)] : MetrizableSpace (∀ i, A i) :=
  by
  cases nonempty_fintype ι
  letI := fun i => metrizableSpaceMetric (A i)
  infer_instance

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