codisjoint_right_comm — Mathlib

English

Let α be a lattice-ordered set with join and a top element. Then for all a, b, c in α, Codisjoint (a ⊔ b) c holds if and only if Codisjoint (a ⊔ c) b holds.

Русский

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

LaTeX

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

Lean4

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

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