mapsTo_swap_prod — Mathlib

English

For any sets s ⊆ α and t ⊆ β, MapsTo Prod.swap (s × t) (t × s) holds, i.e., swapping coordinates maps s × t into t × s.

Русский

Для любых множеств s ⊆ α и t ⊆ β верно, что Prod.swap переводит s × t в t × s.

LaTeX

$$$ \text{MapsTo } Prod.swap (s \timesˢ t) (t \timesˢ s) $$$

Lean4

theorem mapsTo_swap_prod (s : Set α) (t : Set β) : MapsTo Prod.swap (s ×ˢ t) (t ×ˢ s) := fun _ ⟨hx, hy⟩ ↦ ⟨hy, hx⟩

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