snd

Mathlib.Order.Max

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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