biInf_gt_eq_iInf — Mathlib

English

Let α be a complete lattice and ι a type with linear order and NoMinOrder. For any f: ι → α, the infimum over i of the tail infimum over j > i satisfies ⨅_i ⨅_{j>i} f(j) = ⨅_i f(i).

Русский

Пусть α — полная решетка, ι — множество с линейным порядком и без минимального элемента. Для любой f: ι → α выполняется, что инфимум по i от инфимума по j>i равен инфимуму по i: ⨅_i ⨅_{j>i} f(j) = ⨅_i f(i).

LaTeX

$$$\\\\bigwedge_i \\\\bigwedge_{j>i} f(j) = \\\\bigwedge_i f(i)$$$

Lean4

theorem biInf_gt_eq_iInf {ι : Type*} [LT ι] [NoMinOrder ι] {f : ι → α} : ⨅ (i) (j > i), f j = ⨅ i, f i :=
  biInf_lt_eq_iInf (ι := ιᵒᵈ)

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