lowerBounds_prod — Mathlib

English

If s and t are nonempty, then lowerBounds(s × t) = lowerBounds(s) × lowerBounds(t).

Русский

Если множества s и t непусты, то нижние границы их произведения равны произведению нижних границ.

LaTeX

$$$(hs : s.Nonempty) (ht : t.Nonempty) : lowerBounds( s ×ˢ t ) = lowerBounds s ×ˢ lowerBounds t$$$

Lean4

@[simp]
theorem lowerBounds_prod (hs : s.Nonempty) (ht : t.Nonempty) : lowerBounds (s ×ˢ t) = lowerBounds s ×ˢ lowerBounds t :=
  by ext; rw [← nonempty_coe_sort] at hs ht; aesop (add simp [lowerBounds, Prod.le_def, forall_and])

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