sup_left' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sup_left' (h : Codisjoint a b) : Codisjoint (c ⊔ a) b :=
  h.mono_left le_sup_right

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