map_mk

Mathlib.Data.Sigma.Basic

URI: https://scilib.ai/kg/mathlib#Sigma.map_mk

Lean4

theorem map_mk (f₁ : α₁ → α₂) (f₂ : ∀ a, β₁ a → β₂ (f₁ a)) (x : α₁) (y : β₁ x) : map f₁ f₂ ⟨x, y⟩ = ⟨f₁ x, f₂ x y⟩ :=
  rfl

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

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

Разделы

Аффилиация

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