continuous_extensionValuation

Mathlib.Topology.Algebra.Valued.ValuedField

URI: https://scilib.ai/kg/mathlib#Valued.continuous_extensionValuation

English

The extensionValuation map on hat K is continuous.

Русский

Расширенная карта extensionValuation на hat K непрерывна.

LaTeX

$$$Continuous(Valued.extensionValuation)$$$

Lean4

theorem continuous_extensionValuation : Continuous (Valued.extensionValuation : hat K → Γ₀) :=
  continuous_extension

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

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

Разделы

Аффилиация

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