sup_right — Mathlib

English

If a and b are codisjoint, then for any c we have Codisjoint a (b ⊔ c); codisjoint is preserved by right join.

Русский

Если a и b кодиссоединены, то для любого c имеем Codisjoint a (b ⊔ c); кодиссоединение сохраняется справа при объединении с c.

LaTeX

$$$Codisjoint a b \rightarrow Codisjoint a (b \sqcup c)$$$

Lean4

theorem sup_right (h : Codisjoint a b) : Codisjoint a (b ⊔ c) :=
  h.mono_right le_sup_left

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