isRegular_of_decidable

Mathlib.Order.Heyting.Regular

URI: https://scilib.ai/kg/mathlib#Heyting.isRegular_of_decidable

← MathLib Explorer

English

A decidable proposition p is regular, i.e., p ↔ ¬¬p.

Русский

Решаемое высказывание p является регулярным, то есть p ↔ ¬¬p.

LaTeX

$$$(Decidable\ p) \Rightarrow (p \iff \neg\neg p)$$$

Lean4

/-- A decidable proposition is intuitionistically Heyting-regular. -/
theorem isRegular_of_decidable (p : Prop) [Decidable p] : IsRegular p :=
  propext <| Decidable.not_not

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

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

Разделы

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

Аффилиация

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