proj_bot_injective

Mathlib.Topology.DiscreteQuotient

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

English

Under discrete topology, the bottom projection is injective.

Русский

При дискретной топологии нижняя проекция инъективна.

LaTeX

$$$$\\text{[DiscreteTopology X]} \\Rightarrow \\text{Injective}((\\bot : DQ(X)).proj).$$$$

Lean4

theorem proj_bot_injective [DiscreteTopology X] : Injective (⊥ : DiscreteQuotient X).proj := fun _ _ => proj_bot_inj.1

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

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

Разделы

Аффилиация

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