toEncodable

Mathlib.Data.Set.Countable

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

← MathLib Explorer

English

From a countable set s, one can obtain an Encodable structure on s.

Русский

Из счётного множества s можно получить структуру Encodable на s.

LaTeX

$$$\mathrm{toEncodable}(s) : \mathrm{Encodable}(s)$$$

Lean4

/-- Convert `Set.Countable s` to `Encodable s` (noncomputable). -/
protected def toEncodable {s : Set α} (hs : s.Countable) : Encodable s :=
  Classical.choice hs.nonempty_encodable

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

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

Разделы

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

Аффилиация

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