himp_left_comm

Mathlib.Order.Heyting.Basic

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

English

For any a, b, c in α, a → (b → c) = b → (a → c).

Русский

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

LaTeX

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

Lean4

/-- `p → q → r ↔ q → p → r` -/
theorem himp_left_comm (a b c : α) : a ⇨ b ⇨ c = b ⇨ a ⇨ c := by simp_rw [himp_himp, inf_comm]

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

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

Разделы

Аффилиация

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