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 left-multiplication by a is a·b; i.e. sup{a·x : x ∈ s} = a·(sup s).
Русский
Пусть α — упорядоченное полное кольцо; если a ≥ 0 и b является наименьшей верхней гранью (supremum) множества s, то наименьшая верхняя грань образа s при левоумножении на a равна a·b; то есть sup{a·x : x ∈ s} = a·sup s.
LaTeX
$$$(0 \le a) \wedge (\,\sup s = b\,) \Rightarrow \sup\{a x : x \in s\} = a b$$$
Lean4
theorem mul_left {s : Set α} (ha : 0 ≤ a) (hs : IsLUB s b) : IsLUB ((fun b => a * b) '' s) (a * b) :=
by
obtain ha | rfl := ha.lt_or_eq
· exact (OrderIso.mulLeft₀ _ ha).isLUB_image'.2 hs
· simp_rw [zero_mul]
obtain rfl | ne := s.eq_empty_or_nonempty
· simp only [Set.image_empty, isLUB_empty_iff] at hs ⊢
have hb := hs (b + b)
rw [le_add_iff_nonneg_right] at hb
exact hs.mono hb
rw [ne.image_const]
exact isLUB_singleton
