instR1SpaceForall

Mathlib.Topology.Separation.Basic

URI: https://scilib.ai/kg/mathlib#instR1SpaceForall

English

If X and Y are R1 spaces, then the product space X × Y is R1.

Русский

Если X и Y — R1-пространства, то произведение X × Y также является R1-пространством.

LaTeX

$$R1Space(Prod X Y)$$

Lean4

instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, R1Space (X i)] : R1Space (∀ i, X i) :=
  .iInf fun _ ↦ .induced _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru