himp_himp

Mathlib.Order.Heyting.Basic

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

← MathLib Explorer

English

p → q → r is equivalent to p ∧ q → r.

Русский

p → q → r эквивалентно p ∧ q → r.

LaTeX

$$$ a \to b \to c = a \land b \to c $$$

Lean4

/-- `p → q → r ↔ p ∧ q → r` -/
theorem himp_himp (a b c : α) : a ⇨ b ⇨ c = a ⊓ b ⇨ c :=
  eq_of_forall_le_iff fun d => by simp_rw [le_himp_iff, inf_assoc]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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