iSup_range_of_eq_top — Mathlib

English

The direct limit of a directed system is the union of the images of all its component embeddings; in particular, the supremum of the ranges of these embeddings equals the whole direct limit.

Русский

Предел последовательности направленного типа есть объединение образов всех компонентов; сумма образов вложений порождает весь предел.

LaTeX

$$$\big\vee_i\operatorname{range}\big((\mathrm{of}\,L\iota G f i)^{\!\toHom}\big) = \top.$$$

Lean4

theorem iSup_range_of_eq_top : ⨆ i, (of L ι G f i).toHom.range = ⊤ :=
  eq_top_iff.2
    (fun x _ ↦
      DirectLimit.inductionOn x
        (fun i _ ↦ le_iSup (fun i ↦ Hom.range (Embedding.toHom (of L ι G f i))) i (mem_range_self _)))

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