sups_assoc — Mathlib

English

Let α be a semilattice with join and s, t, u Finsets of α. The operation of taking pairwise sup on Finsets, denoted ⊻, is associative: (s ⊻ t) ⊻ u = s ⊻ (t ⊻ u).

Русский

Пусть α — полупорядоченная решетка с операцией объединения ⊔, а s, t, u — конечные множества в α. Операция s ⊻ t — попарный максимум, тогда (s ⊻ t) ⊻ u = s ⊻ (t ⊻ u).

LaTeX

$$$ (s \sqcup t) \sqcup u = s \sqcup (t \sqcup u) $$$

Lean4

theorem sups_assoc : s ⊻ t ⊻ u = s ⊻ (t ⊻ u) :=
  image₂_assoc sup_assoc

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