top_himp

Mathlib.Order.Heyting.Basic

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

English

⊤ → a equals a.

Русский

⊤ → a равняется a.

LaTeX

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

Lean4

@[simp]
theorem top_himp : ⊤ ⇨ a = a :=
  eq_of_forall_le_iff fun b => by rw [le_himp_iff, inf_top_eq]

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

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

Разделы

Аффилиация

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