singleton_union

Mathlib.Data.Set.Insert

URI: https://scilib.ai/kg/mathlib#Set.singleton_union

English

The union of {a} with s is equal to insert a s.

Русский

Объединение {a} с s равно insert a s.

LaTeX

$$@[simp]\\nTheorem: { a } ∪ s = insert a s$$

Lean4

@[simp]
theorem singleton_union : { a } ∪ s = insert a s :=
  rfl

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

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

Разделы

Аффилиация

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