subset_upperBounds_mul — Mathlib

English

Let M be a ordered multiplicative structure with monotone multiplication. For any two sets s and t in M, if u is an upper bound of s and v is an upper bound of t, then the product uv is an upper bound of s t.

Русский

Пусть M — упорядоченная моноидальная структура; для множества s и t в M, если u — верхняя граница s, а v — верхняя граница t, то произведение uv является верхней границей множества s t.

LaTeX

$$$\operatorname{UpperBounds}(s) * \operatorname{UpperBounds}(t) \subseteq \operatorname{UpperBounds}(s t)$$$

Lean4

@[to_additive]
theorem subset_upperBounds_mul (s t : Set M) : upperBounds s * upperBounds t ⊆ upperBounds (s * t) :=
  image2_subset_iff.2 fun _ hx _ hy => mul_mem_upperBounds_mul hx hy

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