in₁

Mathlib.Data.Sum.Basic

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

English

Definition: in1 is the natural inclusion of the second summand into α ⊕ (β ⊕ γ).

Русский

Определение: in1 — естественное включение второго сомножителя в α ⊕ (β ⊕ γ).

LaTeX

$$in1(b) = inr (inl(b))$$

Lean4

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

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

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

Разделы

Аффилиация

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