measurable_coe

Mathlib.MeasureTheory.MeasurableSpace.Constructions

URI: https://scilib.ai/kg/mathlib#QuotientGroup.measurable_coe

← MathLib Explorer

English

The natural projection (↑) : G → G ⧸ S is measurable.

Русский

Естественное проецирование (↑) : G → G ⧸ S измеримо.

LaTeX

$$$\\\\operatorname{Measurable}((\\\\uparrow) : G \\\\rightarrow G \\\\backslash S)$$$

Lean4

@[to_additive (attr := measurability)]
theorem measurable_coe {G} [Group G] [MeasurableSpace G] {S : Subgroup G} : Measurable ((↑) : G → G ⧸ S) :=
  measurable_quotient_mk''

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

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

Разделы

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

Аффилиация

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