prod — Mathlib

English

If s nonempty with LUB a and t nonempty with LUB b, then IsLUB(s × t) {(a,b)}.

Русский

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

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 : IsLUB s a) (hb : IsLUB t b) : IsLUB (s ×ˢ t) (a, b) := by
  simp_all +contextual [IsLUB, IsLeast, lowerBounds]

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