Finite products of reindexed families in a lattice

In a SemilatticeInf with OrderTop, Mathlib identifies the finite product of a family with the infimum of its members (CategoryTheory.Limits.CompleteLattice.finite_product_eq_finset_inf). This file records the reindexed form used for Čech complexes: the product of the members f (a j) of a family f, for a : J → ι with J finite, is the infimum of f over the image of a. Hence a property of the nonempty finite infima of f holds for the products f (a 0) × ⋯ × f (a n).

theorem CategoryTheory.Limits.CompleteLattice.finite_product_eq_finset_image_inf {α : Type u} [SemilatticeInf α] [OrderTop α] {ι : Type v} [DecidableEq ι] {J : Type w} [Fintype J] (f : ι → α) (a : J → ι) : (∏ᶜ fun (j : J) => f (a j)) = (Finset.image a Finset.univ).inf f

The finite product of the members f (a j) of a family f is the infimum of f over the image of a. Unlike finite_product_eq_finset_inf, the index type J may live in any universe, as for the products U (a 0) × ⋯ × U (a n) indexed by Fin (n + 1) in Čech complexes.

theorem CategoryTheory.Limits.CompleteLattice.finite_product_of_forall_finset_inf {α : Type u} [SemilatticeInf α] [OrderTop α] {ι : Type v} {p : α → Prop} (f : ι → α) (h : ∀ (s : Finset ι), s.Nonempty → p (s.inf f)) {J : Type w} [Finite J] [Nonempty J] (a : J → ι) : p (∏ᶜ fun (j : J) => f (a j))

A property of the nonempty finite infima of a family f holds for the nonempty finite products of its members f (a j), such as the products f (a 0) × ⋯ × f (a n) in the terms of Čech complexes: such a product is the infimum of f over the image of a.