inf_himp_le

Mathlib.Order.Heyting.Basic

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

English

The inequality a ∧ (a → b) ≤ b holds in any generalized Heyting algebra.

Русский

Неравенство a ∧ (a → b) ≤ b выполняется в любой обобщенной Хейтинговой алгебре.

LaTeX

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

Lean4

/-- `p ∧ (p → q) → q` -/
theorem inf_himp_le : a ⊓ (a ⇨ b) ≤ b := by rw [inf_comm, ← le_himp_iff]

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

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

Разделы

Аффилиация

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