ciInf_div — Mathlib

English

Infimum divided by a fixed element equals the infimum of divisions: (inf_i f(i))/a = inf_i (f(i)/a).

Русский

inf_i f(i) поделить на a равно inf_i (f(i)/a).

LaTeX

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

Lean4

@[to_additive]
theorem ciInf_div (hf : BddBelow (range f)) (a : G) : (⨅ i, f i) / a = ⨅ i, f i / a := by
  simp only [div_eq_mul_inv, ciInf_mul hf]

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