codisjoint_left_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 b (a ⊔ c) holds.

Русский

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

LaTeX

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

Lean4

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

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