sup_div₀ — Mathlib

English

In a linearly ordered group with zero, for a > 0, the division distributes over finite suprema: s.sup f / a = s.sup (f i / a).

Русский

В линейно упорядоченной группе с нулём для a > 0 деление распространяется на конечные супремумы: s.sup f / a = s.sup (f_i / a).

LaTeX

$$$\text{if } a>0:\ \; s^{\;\uparrow} f / a = s^{\;\uparrow} (f(i)/a).$$$

Lean4

theorem sup_div₀ [LinearOrderedCommGroupWithZero G₀] [OrderBot G₀] {a : G₀} (ha : 0 < a) (s : Finset ι) (f : ι → G₀) :
    s.sup f / a = s.sup fun i ↦ f i / a :=
  by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · simp [← show (0 : G₀) = ⊥ from bot_unique zero_le']
  rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_div₀ (ha := ha)]

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