bihimp_inf_bihimp_le_right

Mathlib.Order.SymmDiff

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

English

For a codisjoint pair b,c, the meet of bihimp with a on right is ≤ a.

Русский

Для кодиссоединенной пары b,c, правая часть bihimp не хуже чем a.

LaTeX

$$$ \operatorname{bihimp}(a, b) \wedge \operatorname{bihimp}(a, c) \\leq a $$$

Lean4

theorem bihimp_inf_bihimp_le_right (h : Codisjoint b c) : a ⇔ b ⊓ a ⇔ c ≤ a :=
  h.dual.le_symmDiff_sup_symmDiff_right

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

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

Разделы

Аффилиация

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