prodMk — Mathlib

English

If a and b are minima in their respective preorderings, then their pair (a,b) is a minimum in the product preorder.

Русский

Если a и b являются минимумами в своих порядках, то пара (a,b) является минимумом в произведении.

LaTeX

$$$\\forall {\\alpha : Type*} {\\beta : Type*} [Preorder \\alpha] [Preorder \\beta] {a : \\alpha} {b : \\beta}, IsMin a \\rightarrow IsMin b \\rightarrow IsMin (\\fst := a, \\snd := b)$$$

Lean4

theorem prodMk (ha : IsMin a) (hb : IsMin b) : IsMin (a, b) := fun _ hc => ⟨ha hc.1, hb hc.2⟩

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