sup_right — Mathlib

English

Let a, b, c be elements of a distributive lattice with bottom. If a is disjoint from b and from c, then a is disjoint from b ⊔ c.

Русский

Пусть a, b, c — элементы распределённой решётки с нулём. Если a ⊥ b и a ⊥ c, то a ⊥ (b ⊔ c).

LaTeX

$$$\operatorname{Disjoint}(a,b) \to \operatorname{Disjoint}(a,c) \to \operatorname{Disjoint}(a, b \sqcup c)$$$

Lean4

theorem sup_right (hb : Disjoint a b) (hc : Disjoint a c) : Disjoint a (b ⊔ c) :=
  disjoint_sup_right.2 ⟨hb, hc⟩

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