pseudoMetrizableSpace_pi — Mathlib

English

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

Русский

Если каждый A_i псевдометризуем, то пространство функций ∀ i A_i псевдометризуемо.

LaTeX

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

Lean4

instance pseudoMetrizableSpace_pi [∀ i, PseudoMetrizableSpace (A i)] : PseudoMetrizableSpace (∀ i, A i) :=
  by
  cases nonempty_fintype ι
  letI := fun i => pseudoMetrizableSpacePseudoMetric (A i)
  infer_instance

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