toWeakDualBCNN_continuous

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

URI: https://scilib.ai/kg/mathlib#MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuous

← MathLib Explorer

English

The map μ ↦ μ.toWeakDualBCNN is continuous.

Русский

Отображение μ ↦ μ.toWeakDualBCNN непрерывно.

LaTeX

$$$\\text{Continuous } (\\text{toWeakDualBCNN})$$$

Lean4

theorem toWeakDualBCNN_continuous : Continuous fun μ : ProbabilityMeasure Ω ↦ μ.toWeakDualBCNN :=
  FiniteMeasure.toWeakDualBCNN_continuous.comp toFiniteMeasure_continuous

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

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

Разделы

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

Аффилиация

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