himp_le_of_right_le

Mathlib.Order.Heyting.Basic

URI: https://scilib.ai/kg/mathlib#Codisjoint.himp_le_of_right_le

← MathLib Explorer

English

If codisjoint a c and b ≤ a, then c → b ≤ a.

Русский

Если Codisjoint a c и b ≤ a, то c ⇨ b ≤ a.

LaTeX

$$$ (hac : Codisjoint a c) \Rightarrow (hba : b \le a) \Rightarrow c \to b \le a $$$

Lean4

/-- See `himp_le` for a stronger version in Boolean algebras. -/
theorem himp_le_of_right_le (hac : Codisjoint a c) (hba : b ≤ a) : c ⇨ b ≤ a :=
  (himp_le_himp_left hba).trans_eq hac.himp_eq_right

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

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

Разделы

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

Аффилиация

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