English
Let α,β be complete lattices and f preserves finite infima (InfTopHom). For finite s and g: s → α, we have f( inf_{x∈s} g(x) ) = inf_{x∈s} f(g(x)).
Русский
Пусть α,β – полные решетки, а f сохраняет конечные нижние пределы. Тогда для любой конечной множества s и функции g: s → α выполняется f( inf_{x∈s} g(x) ) = inf_{x∈s} f(g(x)).
LaTeX
$$$s\text{ finite} \Rightarrow f\big(\bigwedge_{x \in s} g(x)\big) = \bigwedge_{x \in s} f(g(x)).$$$
Lean4
theorem map_finite_biInf {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β] [InfTopHomClass F α β]
{s : Set ι} (hs : s.Finite) (f : F) (g : ι → α) : f (⨅ x ∈ s, g x) = ⨅ x ∈ s, f (g x) :=
by
have := map_finset_inf f hs.toFinset g
simp only [Finset.inf_eq_iInf, hs.mem_toFinset, comp_apply] at this
exact this
