map_le_map

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#OmegaCompletePartialOrder.Chain.map_le_map

English

Another variant of the identity-preservation: c.map OrderHom.id = c.

Русский

Ещё одно свойство тождества для отображения: c.map OrderHom.id = c.

LaTeX

$$$ c.map OrderHom.id = c $$$

Lean4

@[mono]
theorem map_le_map {g : α →o β} (h : f ≤ g) : c.map f ≤ c.map g := fun i => by simp only [map_coe, Function.comp_apply];
  exists i; apply h

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

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

Разделы

Аффилиация

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