English
For a function f: ι → α and an index i, the value partialSups f i equals the supremum of f(j) over all j with j ≤ i; i.e., partialSups f i = sup{ f(j) : j ≤ i }.
Русский
Для функции f: ι → α и индекса i значение partialSups f i равно верхней границе всех f(j) при j ≤ i; то есть partialSups f i = sup{ f(j) : j ≤ i }.
LaTeX
$$$\partialSups f i = \bigvee_{j \le i} f(j)$$$
Lean4
theorem partialSups_eq_ciSup_Iic [ConditionallyCompleteLattice α] (f : ι → α) (i : ι) :
partialSups f i = ⨆ i : Set.Iic i, f i :=
by
simp only [partialSups_apply]
apply le_antisymm
·
exact
sup'_le _ _ fun j hj ↦
le_ciSup_of_le (Set.finite_range _).bddAbove ⟨j, by simpa only [Set.mem_Iic, mem_Iic] using hj⟩ le_rfl
· exact ciSup_le fun ⟨j, hj⟩ ↦ le_sup' f (by simpa only [mem_Iic, Set.mem_Iic] using hj)
