bihimp_inf_bihimp_le_left

Mathlib.Order.SymmDiff

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

English

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

Русский

Для кодиссоединенной пары a,b, наименьшее значение bihimp с c слева не больше чем c.

LaTeX

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

Lean4

theorem bihimp_inf_bihimp_le_left (h : Codisjoint a b) : a ⇔ c ⊓ b ⇔ c ≤ c :=
  h.dual.le_symmDiff_sup_symmDiff_left

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

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

Разделы

Аффилиация

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