English
Let α be a Generalized Boolean Algebra and ι a linearly ordered locally finite order with a bottom element. For any two functions f, d : ι → α, if d is pairwise disjoint and the sequence of partial suprema of d equals that of f, then d is equal to the disjointed sequence of f.
Русский
Пусть α — обобщённая булева алгебра, а ι — линейно упорядоченный локально конечный порядок с нулём. Для любых функций f, d : ι → α, если d попарно взаимно несовместна и частичные верхние пределы d совпадают с частичными верхними пределами f, то d равно disjointed f.
LaTeX
$$$\\forall f\,d : ι \\to α,\; \\bigl(\\operatorname{Pairwise}(\\operatorname{Disjoint} \\text{ on } d)\\bigr) \\rightarrow \\bigl(\\operatorname{partialSups} d = \\operatorname{partialSups} f\\bigr) \\rightarrow d = \\operatorname{disjointed} f$$$
Lean4
/-- `disjointed f` is the unique sequence that is pairwise disjoint and has the same partial sups
as `f`. -/
theorem disjointed_unique' {f d : ι → α} (hdisj : Pairwise (Disjoint on d)) (hsups : partialSups d = partialSups f) :
d = disjointed f :=
disjointed_unique (fun hij ↦ hdisj hij.ne) hsups
