insert

Mathlib.Data.Set.Countable

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

English

If s is countable, then inserting any element a yields a countable set.

Русский

Если s счетно, то вставка любого элемента a дает счетное множество.

LaTeX

$$$\\operatorname{Countable}(s) \\Rightarrow \\operatorname{Countable}(\\operatorname{insert}(a,s))$$$

Lean4

protected theorem insert {s : Set α} (a : α) (h : s.Countable) : (insert a s).Countable :=
  countable_insert.2 h

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

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

Разделы

Аффилиация

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