English
For i ∈ ι, the element sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) belongs to the i-th Cofinal set 𝒟 i.
Русский
Для любого i из индекса i элемент sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) принадлежит i-му кофинальному множеству 𝒟 i.
LaTeX
$$$\\text{Encode\_mem}(i):\\ sequenceOfCofinals\\, p\\, 𝒟\\ (Encodable.encode\\, i + 1) \\in 𝒟 i$$$
Lean4
theorem encode_mem (i : ι) : sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) ∈ 𝒟 i :=
by
dsimp only [sequenceOfCofinals, Nat.add]
rw [Encodable.encodek]
apply Cofinal.above_mem