le_iInf_iff — Mathlib

English

For any f : ι → α and a ∈ α, a ≤ iInf f if and only if a ≤ f i for all i.

Русский

Для любой f : ι → α и элемента a, a ≤ iInf f тогда же и только тогда, когда a ≤ f(i) для всех i.

LaTeX

$$$\\\\forall {f : ι \\\\to α} {a : α}, \\\\left( a \\\\le iInf f \\\\right) \\\\Leftrightarrow \\\\forall i, a \\\\le f(i)$$$

Lean4

@[simp]
theorem le_iInf_iff : a ≤ iInf f ↔ ∀ i, a ≤ f i :=
  (le_isGLB_iff isGLB_iInf).trans forall_mem_range

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