sup_right' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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