prodMk — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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