closure_range — Mathlib

English

For an AbstractCompletion package with a dense embedding, closure of the range of the embedding equals the whole space.

Русский

Для абстрактного завершения с плотной вложенностью замыкание образа вложения равно всему пространству.

LaTeX

$$$\\overline{\\mathrm{range}(\\iota)} = \\mathrm{univ}$$$

Lean4

theorem closure_range : closure (range ι) = univ :=
  pkg.dense.closure_range

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