proj_bot_bijective

Mathlib.Topology.DiscreteQuotient

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

English

The bottom projection is bijective: it is both injective and surjective.

Русский

Нижняя проекция биективна: она и инъективна, и сюръективна.

LaTeX

$$$$\\text{Bijective}((\\bot : DQ(X)).proj).$$$$

Lean4

theorem proj_bot_bijective [DiscreteTopology X] : Bijective (⊥ : DiscreteQuotient X).proj :=
  ⟨proj_bot_injective, proj_surjective _⟩

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

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

Разделы

Аффилиация

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