fst

Mathlib.Order.Max

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

English

If x = (a,b) is maximal, then a is maximal in the first coordinate.

Русский

Если x = (a,b) максимален, то a максимален в первой координате.

LaTeX

$$$\\forall {\\alpha : Type*} {\\beta : Type*} [Preorder \\alpha] [Preorder \\beta] {x : \\Prod \\alpha \\beta}, IsMax x \\rightarrow IsMax x.1$$$

Lean4

theorem fst (hx : IsMax x) : IsMax x.1 := fun c hc => (hx <| show x ≤ (c, x.2) from (and_iff_left le_rfl).2 hc).1

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

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

Разделы

Аффилиация

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