to_countable

Mathlib.Data.Set.Countable

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

English

The elements of s are pairs (x,h) where x ∈ α and h is a proof that x ∈ s.

Русский

Элементы множества s — пары (x,h), где x ∈ α и h — доказательство того, что x ∈ s.

LaTeX

$$$\mathrm{Elem}(s) = \{ (x,h) \mid x \in \alpha \land h : x \in s \}$$$

Lean4

/-- Prove `Set.Countable` from a `Countable` instance on the subtype. -/
theorem to_countable (s : Set α) [Countable s] : s.Countable :=
  ‹_›

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

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

Разделы

Аффилиация

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