sumLexLift_inl_inl

Mathlib.Data.Sum.Interval

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

English

The sumLexLift evaluated at inl a and inl b equals map inl of f1 a b.

Русский

sumLexLift(inl a)(inl b) = map inl (f1 a b).

LaTeX

$$sumLexLift f1 f2 g1 g2 (inl a) (inl b) = (f1 a b).map Embedding.inl$$

Lean4

@[simp]
theorem sumLexLift_inl_inl (a : α₁) (b : β₁) : sumLexLift f₁ f₂ g₁ g₂ (inl a) (inl b) = (f₁ a b).map Embedding.inl :=
  rfl

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

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

Разделы

Аффилиация

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