sup_idem — Mathlib

English

The join operation on CauSeq is idempotent: taking the supremum (join) of a sequence with itself returns the same sequence.

Русский

Объединение двух одинаковых последовательностей CauSeq дает ту же последовательность; операция наибольшего/объединения идемпотентна.

LaTeX

$$$\forall a \in \mathrm{CauSeq}(\alpha, \mathrm{abs})\, (a \vee a = a)$$$

Lean4

@[simp]
protected theorem sup_idem (a : CauSeq α abs) : a ⊔ a = a :=
  Subtype.ext (sup_idem _)

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