surjective

Mathlib.Topology.UniformSpace.Equiv

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

English

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

Русский

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

LaTeX

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

Lean4

protected theorem surjective (h : α ≃ᵤ β) : Function.Surjective h :=
  h.toEquiv.surjective

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

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

Разделы

Аффилиация

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