coe_iInf — Mathlib

English

The coercion of an infimum over a family of order-preserving maps equals the infimum of their coerced values.

Русский

Приведение инфимума над семейством отображений равняется инфимума по приведенным значениям.

LaTeX

$$$((\inf_i f_i) : \text{domain} \to \text{codomain}) = \inf_i (f_i).$$$

Lean4

@[simp, norm_cast]
theorem coe_iInf {ι : Sort*} [CompleteLattice β] (f : ι → α →o β) :
    ((⨅ i, f i : α →o β) : α → β) = ⨅ i, (f i : α → β) := by funext x; simp [iInf_apply]

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