small_insert

Mathlib.Logic.Small.Set

URI: https://scilib.ai/kg/mathlib#small_insert

English

If s is small, then insert x into s is small.

Русский

Если s малое, то вставка x в s тоже малaя.

LaTeX

$$$\operatorname{Small}(s) \Rightarrow \operatorname{Small}(\mathrm{insert}(x, s))$$$

Lean4

instance small_insert (x : α) (s : Set α) [Small.{u} s] : Small.{u} (insert x s : Set α) :=
  Set.insert_eq x s ▸ small_union.{u} { x } s

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

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

Разделы

Аффилиация

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