himp_idem

Mathlib.Order.Heyting.Basic

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

English

For all a, b in α, b → (b → a) = b → a.

Русский

Для всех a, b ∈ α выполняется b ⇨ (b ⇨ a) = b ⇨ a.

LaTeX

$$$ b \to (b \to a) = b \to a $$$

Lean4

@[simp]
theorem himp_idem : b ⇨ b ⇨ a = b ⇨ a := by rw [himp_himp, inf_idem]

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

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

Разделы

Аффилиация

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