fst

Mathlib.Order.Hom.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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