measure_pos_of_nonempty_interior

Mathlib.MeasureTheory.Measure.OpenPos

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.measure_pos_of_nonempty_interior

← MathLib Explorer

English

If interior(s) is nonempty, then μ(s) > 0.

Русский

Если interior(s) непусто, то μ(s) > 0.

LaTeX

$$$(\operatorname{interior} s).\Nonempty \Rightarrow μ(s) > 0.$$$

Lean4

theorem measure_pos_of_nonempty_interior (h : (interior s).Nonempty) : 0 < μ s :=
  (isOpen_interior.measure_pos μ h).trans_le (measure_mono interior_subset)

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

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

Разделы

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

Аффилиация

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