t2Space

Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual

URI: https://scilib.ai/kg/mathlib#SeparatingDual.t2Space

← MathLib Explorer

English

If R is T2, then V is T2 under SeparatingDual R V.

Русский

Если R — T2, то V — T2 при условии SeparatingDual R V.

LaTeX

$$SeparatingDual Real V ⟹ t2Space V$$

Lean4

protected theorem t2Space [T2Space R] : T2Space V :=
  by
  apply (t2Space_iff _).2 (fun {x} {y} hxy ↦ ?_)
  rcases exists_separating_of_ne (R := R) hxy with ⟨f, hf⟩
  exact separated_by_continuous f.continuous hf

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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