English
Let p be a predicate on an index set ι and f a function from the dependent subtype {i ∈ ι | p i} to α, where α is a ConditionallyCompleteLattice. If p i holds for every i, then the infimum of the values f(i, h) over all i ∈ ι and all proofs h of p i equals the infimum of f over the entire subtype {x : p x}. In symbols, if ∀ i, p i, then ⨅ (i) (h : p i), f ⟨i, h⟩ = iInf f.
Русский
Пусть p — свойство на индексовом множестве ι, и пусть f: Subtype p → α, где α — частично упорядкованная решетка, условно полный. Если для каждого i выполняется p i, то инфиму́м по всем парам (i, доказательство p i) от функции f совпадает с инфиму́мом по всей подтиповой функции f.
LaTeX
$$$\text{If }\forall i,\ p(i)\text{ holds, then } \inf_{i: ι}\inf_{h: p(i)} f(\langle i,h\rangle) = \inf_{x: \mathrm{Subtype}(p)} f(x).$$$
Lean4
theorem cbiInf_eq_of_forall {p : ι → Prop} {f : Subtype p → α} (hp : ∀ i, p i) : ⨅ (i) (h : p i), f ⟨i, h⟩ = iInf f :=
cbiSup_eq_of_forall (α := αᵒᵈ) hp
