English
If α is a complete lattice and f: β → α, then the supremum of f over all decode₂ β i, for i ∈ ℕ, equals the supremum over all b ∈ β of f(b): ⨆ i (b ∈ decode₂ β i), f(b) = ⨆ b, f(b).
Русский
Пусть α — полная полуспидость и f: β → α. Тогда наибольшая верхняя грань функции f по всем кодировкам decode₂ β i равна наибольшей верхней грани по всем b ∈ β: ⨆ i (b ∈ decode₂ β i), f(b) = ⨆ b, f(b).
LaTeX
$$$ \\big\\lVert \\!\\!\\! \\big\\rVert = \\big\\vee_{i \\in \\mathbb{N}} \\bigvee_{b \\in decode_2(\\beta,i)} f(b) = \\bigvee_{b \\in \\beta} f(b). $$$
Lean4
theorem iSup_decode₂ [CompleteLattice α] (f : β → α) : ⨆ (i : ℕ) (b ∈ decode₂ β i), f b = (⨆ b, f b) :=
by
rw [iSup_comm]
simp only [mem_decode₂, iSup_iSup_eq_right]
