encode_sigma_val

Mathlib.Logic.Encodable.Basic

URI: https://scilib.ai/kg/mathlib#Encodable.encode_sigma_val

English

The encoding for Sigma γ satisfies: encode of ⟨a,b⟩ equals pair (encode a) (encode b).

Русский

Кодирование Sigma γ удовлетворяет: encode ⟨a,b⟩ = pair (encode a) (encode b).

LaTeX

$$$ \mathrm{encode}(\langle a,b\rangle) = \mathrm{pair}(\mathrm{encode}(a), \mathrm{encode}(b))$$$

Lean4

@[simp]
theorem encode_sigma_val (a b) : @encode (Sigma γ) _ ⟨a, b⟩ = pair (encode a) (encode b) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru