himp_triangle

Mathlib.Order.Heyting.Basic

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

← MathLib Explorer

English

In α, (a → b) ∧ (b → c) ≤ a → c.

Русский

В α выполняется (a ⇨ b) ∧ (b ⇨ c) ≤ a ⇨ c.

LaTeX

$$$ (a \to b) \wedge (b \to c) \le a \to c $$$

Lean4

theorem himp_triangle (a b c : α) : (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c :=
  by
  rw [le_himp_iff, inf_right_comm, ← le_himp_iff]
  exact himp_inf_le.trans le_himp_himp

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

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

Разделы

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

Аффилиация

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