prodMk — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem prodMk (ha : IsTop a) (hb : IsTop b) : IsTop (a, b) := fun _ => ⟨ha _, hb _⟩

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