coe_iInf — Mathlib

English

For a family f: ι → Con M, the coercion of the indexed infimum equals the infimum of the indexed coercions: ↑(iInf f) = iInf i↦↑(f i).

Русский

Для семейства f: ι → Con M, коэрция iInf f равна инфимумации по i: ↑(iInf f) = iInf i, ↑(f i).

LaTeX

$$$\\uparrow (iInf f) = iInf (\\lambda i. \\uparrow (f i))$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_iInf {ι : Sort*} (f : ι → Con M) : ⇑(iInf f) = ⨅ i, ⇑(f i) := by
  rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]

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