ciSup_div — Mathlib

English

Dividing the supremum by a fixed element equals the supremum of the divisions by that element: (sup_i f(i))/a = sup_i (f(i)/a).

Русский

Разделение на фиксированный элемент сохраняет супремум: (sup_i f(i))/a = sup_i (f(i)/a).

LaTeX

$$$\forall \iota, G,\ [MulRightMono G],\ BddAbove(\mathrm{range}\ f) \Rightarrow \forall a\in G, \big(\sup_i f(i)\big)/a = \sup_i \big(f(i)/a\big)$$$

Lean4

@[to_additive]
theorem ciSup_div (hf : BddAbove (range f)) (a : G) : (⨆ i, f i) / a = ⨆ i, f i / a := by
  simp only [div_eq_mul_inv, ciSup_mul hf]

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