mul_mem_upperBounds_mul — Mathlib

English

If a ∈ upperBounds s and b ∈ upperBounds t, then a · b ∈ upperBounds (s · t).

Русский

Если a ∈ верхних границ s и b ∈ верхних границ t, то a · b ∈ верхних границ (s · t).

LaTeX

$$a ∈ upperBounds(s) → b ∈ upperBounds(t) → a * b ∈ upperBounds(s * t)$$

Lean4

@[to_additive]
theorem mul_mem_upperBounds_mul (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : a * b ∈ upperBounds (s * t) :=
  forall_mem_image2.2 fun _ hx _ hy => mul_le_mul' (ha hx) (hb hy)

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