encode_prod_val — Mathlib

English

Let α and β be types with Encodable instances. For any a ∈ α and b ∈ β, the encoding of the pair (a,b) is the pair of encodings: encode (a,b) = pair (encode a) (encode b).

Русский

Пусть α и β — типы с кодируемостью. Для любых a ∈ α и b ∈ β кодирование пары (a,b) равно паре кодов encode a и encode b: encode (a,b) = pair (encode a) (encode b).

LaTeX

$$$ encode((a,b)) = pair (encode a) (encode b) $$$

Lean4

@[simp]
theorem encode_prod_val (a b) : @encode (α × β) _ (a, b) = pair (encode a) (encode b) :=
  rfl

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