coe_iInf — Mathlib

English

The α-value of the infimum of f(i) over i equals the infimum in α of the α-values f(i).

Русский

Значение в α наименьшей границы по i равно ∧_i (f(i) : α).

LaTeX

$$$\left(\uparrow(\mathrm{iInf} f) : α\right) = \bigwedge_{i} (f(i) : α)$$$

Lean4

@[simp]
theorem coe_iInf {ι} (f : ι → L) : (↑(iInf f) : α) = ⨅ i, (f i : α) := by
  rw [iInf, coe_sInf', iInf_range]
    -- Redeclaring to get proper keys for these instances

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