prodComm_apply — Mathlib

English

Let α and β be types. There is a natural equivalence between α × β and β × α given by swapping the coordinates; for every a ∈ α and b ∈ β, the image of (a,b) is (b,a).

Русский

Пусть α и β — типы. Существует естественное эквивалентное соответствие между α × β и β × α, задаваемое обменом координат; для любых a ∈ α и b ∈ β отображение отправляет (a,b) в (b,a).

LaTeX

$$$$ \\mathrm{prodComm}_{\\alpha,\\beta}(a,b) = (b,a). $$$$

Lean4

@[simp, grind =]
theorem prodComm_apply {α β} (x : α × β) : prodComm α β x = x.swap :=
  rfl

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