English
Let α be a linearly ordered semifield with IsStrictOrderedRing. If a ≥ 0 and b is the greatest lower bound (infimum) of a set s ⊆ α, then the greatest lower bound of the image of s under right-multiplication by a is b·a; i.e. inf{ x·a : x ∈ s } = (inf s)·a.
Русский
Пусть α — упорядоченное поле с упорядочением, обладающее свойством строгой монотонности. Если a ≥ 0 и b является наибольшей нижней гранью (infimum) множества s ⊆ α, тогда наибольшая нижняя грань образа s при правом умножении на a равна b·a; то есть inf{ x·a : x ∈ s } = (inf s)·a.
LaTeX
$$$(0 \le a) \wedge (\,\inf s = b\,) \Rightarrow \inf\{x a : x \in s\} = a b$$$
Lean4
theorem mul_right {s : Set α} (ha : 0 ≤ a) (hs : IsGLB s b) : IsGLB ((fun b => b * a) '' s) (b * a) := by
simpa [mul_comm] using hs.mul_left ha
