mul_mem_lowerBounds_mul — Mathlib

English

Let a be a lower bound of s and b be a lower bound of t. Then the product ab is a lower bound of s t.

Русский

Пусть a — нижняя граница s, и b — нижняя граница t. Тогда произведение ab является нижней границей множества s t.

LaTeX

$$$a \in \mathrm{lowerBounds}(s) \land b \in \mathrm{lowerBounds}(t) \Rightarrow ab \in \mathrm{lowerBounds}(s t)$$$

Lean4

@[to_additive]
theorem mul_mem_lowerBounds_mul (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : a * b ∈ lowerBounds (s * t) :=
  mul_mem_upperBounds_mul (M := Mᵒᵈ) ha hb

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