sumLexLift_inr_inr

Mathlib.Data.Sum.Interval

URI: https://scilib.ai/kg/mathlib#Finset.sumLexLift_inr_inr

English

The value at (inr a, inr b) equals map inr of f2 a b.

Русский

Значение при (inr a, inr b) равно map inr (f2 a b).

LaTeX

$$sumLexLift f1 f2 g1 g2 (inr a) (inr b) = (f2 a b).map ⟨_, inr_injective⟩$$

Lean4

@[simp]
theorem sumLexLift_inr_inr (a : α₂) (b : β₂) :
    sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr b) = (f₂ a b).map ⟨_, inr_injective⟩ :=
  rfl

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

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

Разделы

Аффилиация

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