injective

Mathlib.Topology.UniformSpace.Equiv

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

English

Let h: α ≃ᵤ β be a uniform equivalence. The map h is injective.

Русский

Пусть h: α ≃ᵤ β — равномерное эквивалентство. Отображение h инъективно.

LaTeX

$$$\\forall {\\alpha \\beta} [UniformSpace \\alpha] [UniformSpace \\beta] (h : \\alpha \\simeq_u \\beta),\\; Injective(h)$$$

Lean4

protected theorem injective (h : α ≃ᵤ β) : Function.Injective h :=
  h.toEquiv.injective

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

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

Разделы

Аффилиация

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