codisjoint_assoc — Mathlib

English

Let α be a semilattice with join ⊔ and top. Then for all a, b, c ∈ α, the codisjoint relation satisfies Codisjoint((a ⊔ b), c) if and only if Codisjoint(a, (b ⊔ c)).

Русский

Пусть α обладает полукольцом с операцией объединения ⊔ и верхней границей ⊤. Тогда для любых a, b, c ∈ α выполняется равенство Codisjoint((a ⊔ b), c) ⇔ Codisjoint(a, (b ⊔ c)).

LaTeX

$$$\\operatorname{Codisjoint}((a \\sqcup b), c) \\iff \\operatorname{Codisjoint}(a, (b \\sqcup c)).$$$

Lean4

theorem codisjoint_assoc : Codisjoint (a ⊔ b) c ↔ Codisjoint a (b ⊔ c) :=
  @disjoint_assoc αᵒᵈ _ _ _ _ _

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