mk_surjective

Mathlib.Algebra.Order.Archimedean.Class

URI: https://scilib.ai/kg/mathlib#MulArchimedeanClass.mk_surjective

English

The map mk from M to MulArchimedeanClass M is surjective: every Archimedean class has a representative.

Русский

Отображение mk: M → MulArchimedeanClass M сюрьективно: каждый архимедов класс имеет представителя.

LaTeX

$$Function.Surjective mk$$

Lean4

@[to_additive]
theorem mk_surjective : Function.Surjective <| mk (M := M) :=
  Quotient.mk_surjective

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

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

Разделы

Аффилиация

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