himp_le_himp

Mathlib.Order.Heyting.Basic

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

English

For all a, b, c, d in α, (a ≤ b) and (c ≤ d) imply (b → c) ≤ (a → d).

Русский

Для любых a, b, c, d ∈ α, если a ≤ b и c ≤ d, то b ⇨ c ≤ a ⇨ d.

LaTeX

$$$ (h_1 : a \le b) (h_2 : c \le d) \Rightarrow (b \to c) \le (a \to d) $$$

Lean4

theorem himp_le_himp (hab : a ≤ b) (hcd : c ≤ d) : b ⇨ c ≤ a ⇨ d :=
  (himp_le_himp_right hab).trans <| himp_le_himp_left hcd

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

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

Разделы

Аффилиация

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