in₂

Mathlib.Data.Sum.Basic

URI: https://scilib.ai/kg/mathlib#Sum3.in₂

English

Definition: in2 maps the third summand into α ⊕ (β ⊕ γ).

Русский

Определение: in2 переводит третий сомножитель в α ⊕ (β ⊕ γ).

LaTeX

$$in2(c) = inr (inr(c))$$

Lean4

/-- The map from the third summand into a ternary sum. -/
@[match_pattern, simp, reducible]
def in₂ (c : γ) : α ⊕ (β ⊕ γ) :=
  inr <| inr c

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

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

Разделы

Аффилиация

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