ciInf_le — Mathlib

English

Let ι be finite and f: ι → α. Then the infimum over all j of f(j) is less than or equal to every f(i). In the order dual this is the statement, but in the standard order it says ⨅ j f(j) ≤ f(i) for all i.

Русский

Пусть ι конечно и f: ι → α. Тогда инфimum по всем j удовлетворяет: ⨅ j f(j) ≤ f(i) для каждого i.

LaTeX

$$$\inf_{j} f(j) \le f(i)$$$

Lean4

theorem ciInf_le (i : ι) : ⨅ j, f j ≤ f i :=
  le_ciSup (α := αᵒᵈ) f i

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