English
Let α, β be complete lattices with a Galois insertion gi. For any f : ∀ i, p i → α, if for all i hi we have u(l(f(i, hi))) = f(i, hi), then l( inf_i hi f(i, hi) ) = inf_i hi l( f(i, hi) ).
Русский
Пусть существует Галуа-вставка gi между полными решетками, и дано f(i, hi) ∈ α; если для всех i, hi выполняется u(l(f(i, hi))) = f(i, hi), то l(inf_i hi f(i, hi)) = inf_i hi l(f(i, hi)).
LaTeX
$$$$ l\left( \bigwedge_{i}(\;\bigwedge_{h i} f(i,h i)\;) \right) = \bigwedge_{i}(\;\bigwedge_{h i} l(f(i,h i))\;). $$$$
Lean4
theorem l_biInf_u [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} {p : ι → Prop}
(f : ∀ (i) (_ : p i), β) : l (⨅ (i) (hi), u (f i hi)) = ⨅ (i) (hi), f i hi := by
simp only [iInf_subtype', gi.l_iInf_u]
