prod — Mathlib

English

Same as above, with a prod-structured statement; the LUB of the product is the product of the Lub values.

Русский

Аналогично, для пары множеств верхняя граница произведения равна произведению верхних границ значений.

LaTeX

$$$IsLUB s a \rightarrow IsLUB t b \rightarrow IsLUB (s ×ˢ t) { fst := a, snd := b }$$$

Lean4

theorem prod {b : β} (hs : s.Nonempty) (ht : t.Nonempty) (ha : IsGLB s a) (hb : IsGLB t b) : IsGLB (s ×ˢ t) (a, b) := by
  simp_all +contextual [IsGLB, IsGreatest, upperBounds]

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