sup_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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