English
Let α,β be complete lattices and F a map that preserves finite suprema (i.e., f is a SupBotHom). For any finite set s and any g: s → α, we have f( sup_{x∈s} g(x) ) = sup_{x∈s} f(g(x)).
Русский
Пусть α, β – полные решетки, а f сохраняет конечные верхние пределы. Тогда для любой конечной множности s и любой g: s → α выполняется f( sup_{x∈s} g(x) ) = sup_{x∈s} f(g(x)).
LaTeX
$$$s\text{ finite} \Rightarrow f\big(\bigvee_{x \in s} g(x)\big) = \bigvee_{x \in s} f(g(x)).$$$
Lean4
theorem map_finite_biSup {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β] [SupBotHomClass F α β]
{s : Set ι} (hs : s.Finite) (f : F) (g : ι → α) : f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x) :=
by
have := map_finset_sup f hs.toFinset g
simp only [Finset.sup_eq_iSup, hs.mem_toFinset, comp_apply] at this
exact this
