iSupLift_comp_inclusion — Mathlib

English

Under the same directed system setup as above, the lift map iSupLift followed by the inclusion map equals the original component map f_i: (i → K_i) → B, i.e., the two arrows from K_i to B coincide after lifting and including.

Русский

В той же конфигурации направленной системы удачно выполнится: iSupLift(K,dir,f,hf,T,hT) затем включение (inclusion h) равно f_i, т.е. композиции совпадают.

LaTeX

$$$\big( iSupLift(K, dir, f, hf, T, hT) \big) \circ (\mathrm{inclusion}\, h) = f_i$$$

Lean4

@[simp]
theorem iSupLift_comp_inclusion {i : ι} (h : K i ≤ T) : (iSupLift K dir f hf T hT).comp (inclusion h) = f i :=
  by
  ext
  simp only [NonUnitalAlgHom.comp_apply, iSupLift_inclusion]

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