fst

Mathlib.Order.Max

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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