isInducing

Mathlib.Topology.DenseEmbedding

URI: https://scilib.ai/kg/mathlib#IsDenseInducing.isInducing

English

If i is a dense inducing map, then i is an inducing map.

Русский

Если отображение i является плотным индуциируещим, то оно является индуциирующим.

LaTeX

$$$ IsDenseInducing\\ i \\Rightarrow IsInducing\\ i $$$

Lean4

theorem isInducing (di : IsDenseInducing i) : IsInducing i :=
  di.toIsInducing

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

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

Разделы

Аффилиация

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