prop

Mathlib.Order.Heyting.Regular

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

English

Every element of Regular α is regular in α.

Русский

Каждый элемент в Regular α является регулярным в α.

LaTeX

$$$\forall a:\mathrm{Regular}(\alpha),\mathrm{IsRegular}(a\mathrm{.val})$$$

Lean4

theorem prop : ∀ a : Regular α, IsRegular a.val :=
  Subtype.prop

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

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

Разделы

Аффилиация

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