get_add

Mathlib.Data.Nat.PartENat

URI: https://scilib.ai/kg/mathlib#PartENat.get_add

English

For x,y ∈ PartENat with (x+y).Dom, get (x+y) h = x.get h.1 + y.get h.2.

Русский

Для x,y ∈ PartENat с условием (x+y).Dom, get (x+y) h = x.get h.1 + y.get h.2.

LaTeX

$$@[simp] get_add {x y : PartENat} (h : (x + y).Dom) : get (x + y) h = x.get h.1 + y.get h.2$$

Lean4

@[simp]
theorem get_add {x y : PartENat} (h : (x + y).Dom) : get (x + y) h = x.get h.1 + y.get h.2 :=
  rfl

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

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

Разделы

Аффилиация

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