regularSpace_induced

Mathlib.Topology.Separation.Regular

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

English

If Y has the induced topology from X and X is regular, then Y is regular.

Русский

Если Y имеет индуцированную топологию от X и X регулярное, то Y регулярное.

LaTeX

$$$RegularSpace(X) \Rightarrow RegularSpace(Y)$ для InducedTopology от X$$

Lean4

theorem regularSpace_induced (f : Y → X) : @RegularSpace Y (induced f ‹_›) :=
  letI := induced f ‹_›
  (IsInducing.induced f).regularSpace

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

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

Разделы

Аффилиация

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