English
Let α and β be complete lattices and gi a Galois insertion, and take a function f: ι → β. Then l( inf_i f(i) ) = inf_i f(i) after applying l to the infimum is the infimum of the images. In particular, l(⨅ i, u(f(i))) = ⨅ i, f(i).
Русский
Пусть α, β — полные решетки, gi — Галуа-вставка, имеется функция f: ι → β. Тогда l(инф_i f(i)) = инф_i f(i) с учётом отображения, т.е. l(⨅ i, u(f(i))) = ⨅ i, f(i).
LaTeX
$$$$ l\left( \bigwedge_{i} u\big(f(i)\big) \right) = \bigwedge_{i} f(i). $$$$
Lean4
theorem l_iInf_u [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} (f : ι → β) :
l (⨅ i, u (f i)) = ⨅ i, f i :=
calc
l (⨅ i : ι, u (f i)) = l (u (⨅ i : ι, f i)) := congr_arg l gi.gc.u_iInf.symm
_ = ⨅ i : ι, f i := gi.l_u_eq _
