mem_map_swap

Mathlib.Data.List.ProdSigma

URI: https://scilib.ai/kg/mathlib#List.mem_map_swap

English

For any xs, (y,x) is in map Prod.swap xs iff (x,y) is in xs.

Русский

Для любого xs: (y,x) принадлежит map Prod.swap xs тогда и только тогда, когда (x,y) принадлежит xs.

LaTeX

$$$(y,x) \in map Prod.swap xs \iff (x,y) \in xs$$$

Lean4

@[simp 1100]
theorem mem_map_swap (x : α) (y : β) (xs : List (α × β)) : (y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs := by simp

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

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

Разделы

Аффилиация

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