mul_left — Mathlib

English

If a ≥ 0 and b is the greatest lower bound of a set s, then a · b is the greatest lower bound of a·s.

Русский

Если a ≥ 0 и b — наибольшая нижняя грань множества s, то a b — наибольшая нижняя грань множества a·s.

LaTeX

$$$0 \le a \Rightarrow IsGLB\, s\, b \Rightarrow IsGLB\, ((\lambda x. a \cdot x) '' s)\, (a \cdot b)$$$

Lean4

theorem mul_left {s : Set α} (ha : 0 ≤ a) (hs : IsGLB s b) : IsGLB ((fun b => a * b) '' s) (a * b) :=
  by
  rcases lt_or_eq_of_le ha with (ha | rfl)
  · exact (OrderIso.mulLeft₀ _ ha).isGLB_image'.2 hs
  · simp_rw [zero_mul]
    rw [hs.nonempty.image_const]
    exact isGLB_singleton

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