coe_sort_true

Mathlib.Data.Bool.Basic

URI: https://scilib.ai/kg/mathlib#Bool.coe_sort_true

English

The true proposition (as a Prop) equals True.

Русский

Истина как пропозиция равна True.

LaTeX

$$$$ (\mathrm{true} : \mathrm{Prop}) = \mathrm{True}. $$$$

Lean4

theorem coe_sort_true : (true : Prop) = True := by simp

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

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

Разделы

Аффилиация

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