sym2_eq_image — Mathlib

English

The Sym2 set equals the image of the pairing function on the product s × s.

Русский

Сим2-образ равен изображению отображения пары по произведению s × s.

LaTeX

$$s^{(2)} = (s \times s).\mathrm{image} \mathrm{Sym2.mk}$$

Lean4

theorem sym2_eq_image : s.sym2 = (s ×ˢ s).image Sym2.mk :=
  by
  ext z
  refine z.ind fun x y ↦ ?_
  rw [mk_mem_sym2_iff, mem_image]
  constructor
  · intro h
    use (x, y)
    simp only [mem_product, h, and_self]
  · rintro ⟨⟨a, b⟩, h⟩
    simp only [mem_product, Sym2.eq_iff] at h
    obtain ⟨h, (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)⟩ := h <;> simp [h]

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