continuousOn_div

Mathlib.Topology.Algebra.GroupWithZero

URI: https://scilib.ai/kg/mathlib#continuousOn_div

English

If the same hypotheses hold as in 195292, the units embed topologically.

Русский

Если соблюдены те же условия, что и в 195292, единицы вкладываются топологически.

LaTeX

$$$\\text{IsEmbedding}(\\mathrm{val} : G_0^{\\times} \\to G_0)$$$

Lean4

theorem continuousOn_div : ContinuousOn (fun p : G₀ × G₀ => p.1 / p.2) {p | p.2 ≠ 0} :=
  continuousOn_fst.div continuousOn_snd fun _ => id

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

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

Разделы

Аффилиация

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