nullMeasurableSet_lt'

Mathlib.MeasureTheory.Constructions.BorelSpace.Order

URI: https://scilib.ai/kg/mathlib#nullMeasurableSet_lt'

← MathLib Explorer

English

For μ on α×α, the set {p ∈ α×α | p.1 < p.2} is null‑measurable.

Русский

Для меры μ на α×α множество {p | p1 < p2} нулевеко измеримо.

LaTeX

$$$\text{NullMeasurableSet}\{p\in\alpha\times\alpha\mid p_{1}

Lean4

theorem nullMeasurableSet_lt' [SecondCountableTopology α] {μ : Measure (α × α)} :
    NullMeasurableSet {p : α × α | p.1 < p.2} μ :=
  measurableSet_lt'.nullMeasurableSet

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

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

Разделы

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

Аффилиация

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