of_comp

Mathlib.Topology.Closure

URI: https://scilib.ai/kg/mathlib#DenseRange.of_comp

English

If f ∘ g has dense range, then f has dense range.

Русский

Если образ функции f ∘ g плотен, то образ функции f плотен.

LaTeX

$$$DenseRange (f \circ g) \rightarrow DenseRange f$$$

Lean4

theorem of_comp {α β : Type*} {f : α → X} {g : β → α} (h : DenseRange (f ∘ g)) : DenseRange f :=
  Dense.mono (range_comp_subset_range g f) h

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

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

Разделы

Аффилиация

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