encode_mem — Mathlib

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

Похожие утверждения