iInf_range' — Mathlib

English

For any map g: β → α and f: ι → β, the infimum over the range of f of g is the same as the infimum over i of g(f(i)).

Русский

Для любой функции g: β → α и f: ι → β, инфиму́мум по диапазону f от g равен инфиму́муму по i от g(f(i)).

LaTeX

$$$$\\inf_{b \\in \\operatorname{range}(f)} g(b) = \\inf_{i} g(f(i)).$$$$

Lean4

theorem iInf_range' (g : β → α) (f : ι → β) : ⨅ b : range f, g b = ⨅ i, g (f i) :=
  @iSup_range' αᵒᵈ _ _ _ _ _

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