ofLE_continuous

Mathlib.Topology.DiscreteQuotient

URI: https://scilib.ai/kg/mathlib#DiscreteQuotient.ofLE_continuous

English

If A ≤ B, the induced map from A to B is continuous.

Русский

Если A ≤ B, индуцированное отображение из A в B непрерывно.

LaTeX

$$$$\\forall h : A \\le B,\\; \\mathrm{Continuous}(\\mathrm{ofLE}(h)).$$$$

Lean4

theorem ofLE_continuous (h : A ≤ B) : Continuous (ofLE h) :=
  continuous_of_discreteTopology

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

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

Разделы

Аффилиация

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