coe_iInf — Mathlib

English

The coerced infimum equals the infimum taken in WithBot α for a bounded-below family.

Русский

Приведение к WithBot сохраняет инфимум: ↑(⨅ i, f i) = ⨅ i, f i в WithBot(α).

LaTeX

$$$\uparrow\left(\inf_i f(i)\right) = \inf_i f(i)\quad\text{in } WithBot(\alpha)$$$

Lean4

@[norm_cast]
theorem coe_iInf [InfSet α] (f : ι → α) (h : BddBelow (Set.range f)) : ↑(⨅ i, f i) = (⨅ i, f i : WithBot α) :=
  WithTop.coe_iSup (α := αᵒᵈ) _ h

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