English
Let {K_i} be a directed family of nonunital subalgebras of A over R, with compatible maps f_i : K_i → B and a directed colimit T = iSup K. If hT expresses T as the supremum of the K_i and h provides inclusions K_i ≤ T, then for every i and x ∈ K_i, iSupLift applied to the inclusion map sends x to f_i(x).
Русский
Пусть {K_i} — направленная совокупность ненулевых подполуг A над R, и даны совместимые отображения f_i : K_i → B; T — их супремум T = iSup K. При условии, что hT задаёт равенство T и iSup K и дано включение h: K_i ≤ T, для каждого i и каждого x ∈ K_i выполняется: iSupLift(K, dir, f, hf, T, hT)(inclusion h x) = f_i(x).
LaTeX
$$$\forall i\, (x \in K_i)\, \forall h: K_i \le T,\; iSupLift(K, dir, f, hf, T, hT)(\mathrm{inclusion}\, h\, x) = f_i(x)$$$
Lean4
@[simp]
theorem iSupLift_inclusion {i : ι} (x : K i) (h : K i ≤ T) : iSupLift K dir f hf T hT (inclusion h x) = f i x :=
by
subst T
dsimp [iSupLift]
apply Set.iUnionLift_inclusion
exact h
