insert

Mathlib.Data.Set.Defs

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

← MathLib Explorer

English

Set.insert a s is the set {a} ∪ s.

Русский

Set.insert a s есть множество {a} ∪ s.

LaTeX

$$$\\operatorname{insert}(a,s) = \\{b\\;|\\; b = a \\lor b \\in s\\}$$$

Lean4

/-- `Set.insert a s` is the set `{a} ∪ s`.

Note that you should **not** use this definition directly, but instead write `insert a s` (which is
mediated by the `Insert` typeclass). -/
protected def insert (a : α) (s : Set α) : Set α :=
  {b | b = a ∨ b ∈ s}

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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