sym2_insert — Mathlib

English

The sym2 of inserting a into s equals the union of the image of the map b ↦ s(a,b) applied to insert a s and s.sym2.

Русский

Sym2 от вставки элемента a в s равен объединению образа отображения b ↦ s(a,b) от insert a s и Sym2-образа s.

LaTeX

$$$ (insert\ a\ s).sym2 = \left(\mathrm{image}(\lambda b \mapsto \mathrm{Sym2.mk}(a,b)) (insert\ a\ s)\right) \cup s.\mathrm(sym2) $$$

Lean4

theorem sym2_insert (a : α) (s : Set α) : (insert a s).sym2 = (fun b ↦ s(a, b)) '' insert a s ∪ s.sym2 := by ext ⟨x, y⟩;
  aesop

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