countable'

Mathlib.Data.Countable.Defs

URI: https://scilib.ai/kg/mathlib#Prop.countable'

English

Prop is countable via an equivalence with Bool.

Русский

Prop счётен через эквивелентность с Bool.

LaTeX

$$$\text{Countable}(\text{Prop})$$$

Lean4

instance countable' : Countable Prop :=
  Countable.of_equiv Bool Equiv.propEquivBool.symm

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

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

Разделы

Аффилиация

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