isInducing_mk

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#SeparationQuotient.isInducing_mk

← MathLib Explorer

English

The map mk is inducing.

Русский

Отображение mk является индукционирующим.

LaTeX

$$$\\text{IsInducing}(\\mathrm{mk})$$$

Lean4

theorem isInducing_mk : IsInducing (mk : X → SeparationQuotient X) :=
  ⟨le_antisymm (continuous_iff_le_induced.1 continuous_mk) fun s hs =>
      ⟨mk '' s, isOpenMap_mk s hs, preimage_image_mk_open hs⟩⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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