himp_self

Mathlib.Order.Heyting.Basic

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

English

In a generalized Heyting algebra, a → a equals the top element ⊤.

Русский

В обобщенной Хейтинговой алгебре a → a равняется верхнему элементу ⊤.

LaTeX

$$$ a \to a = \top $$$

Lean4

/-- `p → p` -/
@[simp]
theorem himp_self : a ⇨ a = ⊤ :=
  top_le_iff.1 <| le_himp_iff.2 inf_le_right

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

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

Разделы

Аффилиация

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