measure_ne_zero

Mathlib.MeasureTheory.Measure.OpenPos

URI: https://scilib.ai/kg/mathlib#IsOpen.measure_ne_zero

English

For an open set U that is nonempty, μ(U) ≠ 0.

Русский

Для открытого множества U, не пустого, мера μ(U) не равна нулю.

LaTeX

$$$\text{IsOpen}(U) \wedge U\neq \emptyset \Rightarrow μ(U) \neq 0.$$$

Lean4

theorem _root_.IsOpen.measure_ne_zero (hU : IsOpen U) (hne : U.Nonempty) : μ U ≠ 0 :=
  IsOpenPosMeasure.open_pos U hU hne

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

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

Разделы

Аффилиация

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