himp_le_himp_himp_himp — Mathlib

English

Let α be a generalized Heyting algebra and a, b, c be elements of α. Then b → c ≤ (a → b) → (a → c).

Русский

Пусть α — обобщённая гейтинговая алгебра, и a, b, c ∈ α. Тогда b ⇨ c ≤ (a ⇨ b) ⇨ (a ⇨ c).

LaTeX

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

Lean4

/-- `(q → r) → (p → q) → q → r` -/
theorem himp_le_himp_himp_himp : b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c :=
  by
  rw [le_himp_iff, le_himp_iff, inf_assoc, himp_inf_self, ← inf_assoc, himp_inf_self, inf_assoc]
  exact inf_le_left

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