himp_inf_himp_inf_le

Mathlib.Order.Heyting.Basic

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

English

In a generalized Heyting algebra, (b → c) ∧ (a → b) ∧ a ≤ c for all a, b, c ∈ α.

Русский

В обобщённой гейтинговой алгебре для любых a, b, c ∈ α выполняется (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c.

LaTeX

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

Lean4

@[simp]
theorem himp_inf_himp_inf_le : (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c := by simpa using @himp_le_himp_himp_himp

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

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

Разделы

Аффилиация

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