English
If for each i in I there is a GC between α_i and β_i, then the pointwise maps on the product spaces form a GC between ∀ i, α_i and ∀ i, β_i.
Русский
Если для каждого i в I существуют связи Галуа между α_i и β_i, то поэлементные отображения на произведениях образуют связь Галуа между ∀ i, α_i и ∀ i, β_i.
LaTeX
$$$$ \forall i, GC(l_i,u_i) \Rightarrow GC(\lambda a i, l_i(a_i), \lambda b i, u_i(b_i)). $$$$
Lean4
protected theorem dfun {ι : Type u} {α : ι → Type v} {β : ι → Type w} [∀ i, Preorder (α i)] [∀ i, Preorder (β i)]
(l : ∀ i, α i → β i) (u : ∀ i, β i → α i) (gc : ∀ i, GaloisConnection (l i) (u i)) :
GaloisConnection (fun (a : ∀ i, α i) i => l i (a i)) fun b i => u i (b i) := fun a b =>
forall_congr' fun i => gc i (a i) (b i)
