English
If x lies in the lifted directed system via inclusions, then the iSupLift evaluated at inclusion equals the i-th component.
Русский
Если элемент x принадлежит куче X через включения, то iSupLift на включение совпадает с f_i.
LaTeX
$$$iSupLift\\ K\\ dir\\ f\\ hf\\ T\\ hT\\ (inclusion\\ h\\ x) = f\\ i\\ x$$$
Lean4
theorem coe_iSup_of_directed [Nonempty ι] {S : ι → NonUnitalStarSubalgebra R A} (dir : Directed (· ≤ ·) S) :
↑(iSup S) = ⋃ i, (S i : Set A) :=
let K : NonUnitalStarSubalgebra R A :=
{ __ := NonUnitalSubalgebra.copy _ _ (NonUnitalSubalgebra.coe_iSup_of_directed dir).symm
star_mem' := fun hx ↦
let ⟨i, hi⟩ := Set.mem_iUnion.1 hx
Set.mem_iUnion.2 ⟨i, star_mem (s := S i) hi⟩ }
have : iSup S = K :=
le_antisymm (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set A)) i) (Set.iUnion_subset fun _ ↦ le_iSup S _)
this.symm ▸ rfl
