injective

Mathlib.Topology.Homeomorph.Defs

URI: https://scilib.ai/kg/mathlib#IsHomeomorph.injective

English

If hf is IsHomeomorph, then hf is injective.

Русский

Если hf является IsHomeomorph, то он инъективен.

LaTeX

$$$ \\text{IsHomeomorph.injective}(hf) : \\text{Function.Injective } f $$$

Lean4

protected theorem injective (hf : IsHomeomorph f) : Function.Injective f :=
  hf.bijective.injective

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

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

Разделы

Аффилиация

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