subset_lowerBounds_mul — Mathlib

English

For any sets s,t, the product of their lower bounds is contained in the lower bounds of the product set, i.e., lowerBounds s multiplied by lowerBounds t is contained in lowerBounds (s t).

Русский

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

LaTeX

$$$\mathrm{lowerBounds}(s) * \mathrm{lowerBounds}(t) \subseteq \mathrm{lowerBounds}(s t)$$$

Lean4

@[to_additive]
theorem subset_lowerBounds_mul (s t : Set M) : lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t) :=
  subset_upperBounds_mul (M := Mᵒᵈ) _ _

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