English
If each α(i) carries a locally finite order and ι is finite, then the function space ∀ i, α(i) with the pointwise order is locally finite; in particular the coordinatewise intervals Icc(a,b) form a finite product of the one-dimensional intervals.
Русский
Если каждое α(i) имеет локально конечный порядок и ι конечно, то множество функций ∀ i, α(i) с точечно определённым порядком локально конечно; в частности локальные интервалы координат дают конечное произведение.
LaTeX
$$$$ \\forall i, \\text{LocallyFiniteOrder}(\\alpha(i)) \\Rightarrow \\text{LocallyFiniteOrder}(\\,\\forall i, \\alpha(i)\\,) $$$$
Lean4
instance instLocallyFiniteOrder : LocallyFiniteOrder (∀ i, α i) :=
LocallyFiniteOrder.ofIcc _ (fun a b => piFinset fun i => Icc (a i) (b i)) fun a b x => by
simp_rw [mem_piFinset, mem_Icc, le_def, forall_and]
