natSumNatEquivNat_apply

Mathlib.Logic.Equiv.Nat

URI: https://scilib.ai/kg/mathlib#Equiv.natSumNatEquivNat_apply

English

The equivalence between ℕ ⊕ ℕ and ℕ sends inl x to 2x and inr x to 2x+1.

Русский

Эквивалентность между ℕ ⊕ ℕ и ℕ отправляет inl x в 2x и inr x в 2x+1.

LaTeX

$$$\\text{natSumNatEquivNat}(\\text{inl } x)=2x,\\quad \\text{natSumNatEquivNat}(\\text{inr } x)=2x+1.$$$

Lean4

@[simp]
theorem natSumNatEquivNat_apply : ⇑natSumNatEquivNat = Sum.elim (2 * ·) (2 * · + 1) := by ext (x | x) <;> rfl

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

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

Разделы

Аффилиация

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