map_strictMono_of_injective

Mathlib.ModelTheory.Substructures

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Substructure.map_strictMono_of_injective

English

The map on substructures is strictly monotone when f is injective: map f is StrictMono.

Русский

Отображение map f на подструктуры строго монотонно при инъективности f.

LaTeX

$$$\mathrm{StrictMono}(\mathrm{map}_f)$$$

Lean4

theorem map_strictMono_of_injective : StrictMono (map f) :=
  (gciMapComap hf).strictMono_l

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

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

Разделы

Аффилиация

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