mul_right — Mathlib

English

Let α be a linearly ordered semifield with IsStrictOrderedRing. If a ≥ 0 and b is the least upper bound (supremum) of a set s, then the least upper bound of the image of s under right-multiplication by a is b·a; i.e. sup{ x·a : x ∈ s } = b·a.

Русский

Пусть α — упорядоченное полное кольцо; если a ≥ 0 и b является наименьшей верхней гранью множества s, то sup{ x·a : x ∈ s } = b·a.

LaTeX

$$$(0 \le a) \wedge (\,\sup s = b\,) \Rightarrow \sup\{x a : x \in s\} = b a$$$

Lean4

theorem mul_right {s : Set α} (ha : 0 ≤ a) (hs : IsLUB s b) : IsLUB ((fun b => b * a) '' s) (b * a) := by
  simpa [mul_comm] using hs.mul_left ha

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