prop

Mathlib.Data.Fintype.EquivFin

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

English

Any proposition p is a finite type (the type p has at most one element).

Русский

Любое proposition p является конечным типом (у p не более одного элемента).

LaTeX

$$$\mathrm{Finite}(p) \quad \text{for any } p:\text{Prop}.$$$

Lean4

instance prop (p : Prop) : Finite p :=
  Finite.of_subsingleton

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

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

Разделы

Аффилиация

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