iInf_apply — Mathlib

English

The infimum of a family of order-preserving maps, applied to x, equals the infimum over the index set of the values at x.

Русский

Инфинум семейства отображений применяется к x как инфимум по значениям на x.

LaTeX

$$$(\inf_i f_i)\, x = \inf_i (f_i\, x).$$$

Lean4

theorem iInf_apply {ι : Sort*} [CompleteLattice β] (f : ι → α →o β) (x : α) : (⨅ i, f i) x = ⨅ i, f i x :=
  (sInf_apply _ _).trans iInf_range

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