snd

Mathlib.Order.Hom.Basic

URI: https://scilib.ai/kg/mathlib#OrderHom.snd

English

snd is an order-hom from α × β to β, i.e., projection to the second component preserves order.

Русский

snd — монотонное отображение из α×β в β, проекция на вторую компоненту сохраняет порядок.

LaTeX

$$$ snd: α \times β \to^o β. $$$

Lean4

/-- `Prod.snd` as an `OrderHom`. -/
@[simps]
def snd : α × β →o β :=
  ⟨Prod.snd, fun _ _ h => h.2⟩

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

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

Разделы

Аффилиация

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