dense_iUnion_range_toInductiveLimit

English

The union of the ranges of the maps toInductiveLimit I i is dense in the inductive limit.

Русский

Объединение областей обхода отображений toInductiveLimit I i плотно в инддуктивном пределе.

LaTeX

$$$\overline{\bigcup_{i} \mathrm{range}(\mathrm{toInductiveLimit}\,I\,i)} = \text{Dense in } \operatorname{InductiveLimit}(I)$$$

Lean4

theorem dense_iUnion_range_toInductiveLimit {X : ℕ → Type u} [(n : ℕ) → MetricSpace (X n)]
    {f : (n : ℕ) → X n → X (n + 1)} (I : ∀ (n : ℕ), Isometry (f n)) : Dense (⋃ i, range (toInductiveLimit I i)) :=
  by
  refine dense_univ.mono ?_
  rintro ⟨n, x⟩ _
  refine mem_iUnion.2 ⟨n, mem_range.2 ⟨x, rfl⟩⟩

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