isDenseInducing

Mathlib.Topology.UniformSpace.UniformEmbedding

URI: https://scilib.ai/kg/mathlib#IsUniformInducing.isDenseInducing

English

If f is IsUniformInducing and its range is dense in the target, then f is IsDenseInducing.

Русский

Если f — IsUniformInducing и образ dense в целевом пространстве, то f является IsDenseInducing.

LaTeX

$$$IsDenseInducing f$$$

Lean4

theorem isDenseInducing (h : IsUniformInducing f) (hd : DenseRange f) : IsDenseInducing f
    where
  toIsInducing := h.isInducing
  dense := hd

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru