biInf_ge_eq_iInf — Mathlib

English

For any Preorder ι and f: ι → α, the infimum of all tail values with indices ≥ b equals the value at b, i.e. ⨅_{b' ≥ b} f(b') = f(b).

Русский

Для любого предпорядка ι и функции f: ι → α верно, что инфимум по всем значениям хвоста, индексируемых не меньшими чем b, равен значению в b: ⨅_{b' ≥ b} f(b') = f(b).

LaTeX

$$$\\\\bigwedge_{b' \\\\ge b} f(b') = f(b)$$$

Lean4

theorem biInf_ge_eq_iInf {ι : Type*} [Preorder ι] {f : ι → α} : ⨅ (i) (j ≥ i), f j = ⨅ i, f i :=
  biInf_le_eq_iInf (ι := ιᵒᵈ)

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