English
Let α be a complete lattice, a ∈ α, and for each i in an index set ι pick f(i) ∈ Iic(a). For each i, let p(i) be a proposition. Then the α-value of the infimum over i of the infimum over all witnesses of p(i) of f(i) equals a ∧ the infimum over i of the infimum over witnesses of p(i) of the α-valued f(i).
Русский
Пусть α — полная решетка, a ∈ α, для каждого i из индекса ι выбрать элемент f(i) ∈ Iic(a). Пусть p(i) — некоторое высказывание. Тогда значение в α у наименьшей нижней границы по переменной i от наибольшей нижней границы по witness’ам p(i) от f(i) равно a ∧ ∧_i ∧_{(x : p(i))} (f(i)).
LaTeX
$$$\left(\uparrow\left(\bigwedge_{i} \bigwedge_{(x : p(i))} f(i)\right) : \alpha\right) = a \wedge \bigwedge_{i} \bigwedge_{(x : p(i))} (f(i) : \alpha)$$$
Lean4
theorem coe_biInf : (↑(⨅ i, ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ i, ⨅ (_ : p i), (f i : α) :=
by
cases isEmpty_or_nonempty ι
· simp
· simp_rw [coe_iInf, ← inf_iInf, ← inf_assoc, inf_idem]
