leAdd_apply

Mathlib.Order.InitialSeg

URI: https://scilib.ai/kg/mathlib#InitialSeg.leAdd_apply

English

For any a, leAdd r s a equals Sum.inl a.

Русский

Для любого a, leAdd r s a равно Sum.inl a.

LaTeX

$$$leAdd(r,s)(a) = Sum.inl(a).$$$

Lean4

@[simp]
theorem leAdd_apply (r : α → α → Prop) (s : β → β → Prop) (a) : leAdd r s a = Sum.inl a :=
  rfl

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

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

Разделы

Аффилиация

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