swap₂

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#Function.swap₂

Lean4

/-- Swaps two pairs of arguments to a function. -/
abbrev swap₂ {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*} {φ : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Sort*}
    (f : ∀ i₁ j₁ i₂ j₂, φ i₁ j₁ i₂ j₂) (i₂ j₂ i₁ j₁) : φ i₁ j₁ i₂ j₂ :=
  f i₁ j₁ i₂ j₂

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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