prodMk — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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