measure_pos_iff

Mathlib.MeasureTheory.Measure.OpenPos

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

← MathLib Explorer

English

For open U, 0 < μ(U) iff U is nonempty.

Русский

Для открытого U: 0 < μ(U) тогда и только тогда U непусто.

LaTeX

$$$IsOpen(U) \Rightarrow (0 < μ(U) \iff U \neq \emptyset).$$$

Lean4

theorem _root_.IsOpen.measure_pos_iff (hU : IsOpen U) : 0 < μ U ↔ U.Nonempty :=
  ⟨fun h => nonempty_iff_ne_empty.2 fun he => h.ne' <| he.symm ▸ measure_empty, hU.measure_pos μ⟩

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

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

Разделы

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

Аффилиация

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