coe_iInf — Mathlib

English

The coercion of the infimum equals the infimum taken in WithTop α for a bounded-below family.

Русский

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

LaTeX

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

Lean4

@[norm_cast]
theorem coe_iInf [Nonempty ι] [InfSet α] {f : ι → α} (hf : BddBelow (range f)) : ↑(⨅ i, f i) = (⨅ i, f i : WithTop α) :=
  by rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f) hf, ← range_comp, Function.comp_def]

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