instFirstCountableTopology

Mathlib.Analysis.Distribution.SchwartzSpace

URI: https://scilib.ai/kg/mathlib#SchwartzMap.instFirstCountableTopology

English

SchwartzMap has a first-countable topology induced by its seminorms.

Русский

SchwartzMap имеет топологию первого счетного базиса, индуцированную семинарами.

LaTeX

$$$\text{instFirstCountableTopology}: FirstCountableTopology 𝓢(E,F)$$$

Lean4

instance instFirstCountableTopology : FirstCountableTopology 𝓢(E, F) :=
  (schwartz_withSeminorms ℝ E F).firstCountableTopology

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

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

Разделы

Аффилиация

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