mk_preimage_sym2 — Mathlib

English

Let s be a subset of α. Then the set of all pairs (a,b) with a ∈ s and b ∈ s equals the preimage of s.sym2 under the map mk: α × α → Sym2 α, i.e. Sym2.mk^{-1}(s.sym2) = s × s.

Русский

Пусть s ⊆ α. Тогда множество всех пар (a,b) с a ∈ s и b ∈ s совпадает с предобразом s.sym2 по отображению mk: α × α → Sym2 α; то есть Sym2.mk^{-1}(s.sym2) = s × s.

LaTeX

$$$ (\mathrm{Sym2.mk})^{-1}(s.\mathrm{sym2}) = s \times s $$$

Lean4

@[simp]
theorem mk_preimage_sym2 : Sym2.mk ⁻¹' s.sym2 = s ×ˢ s :=
  rfl

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