measure_ne_top_of_subset

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

URI: https://scilib.ai/kg/mathlib#MeasureTheory.measure_ne_top_of_subset

English

If t ⊆ s and μ(s) ≠ ∞, then μ(t) ≠ ∞.

Русский

Если t ⊆ s и μ(s) ≠ ∞, то μ(t) ≠ ∞.

LaTeX

$$(t ⊆ s) ∧ (μ(s) ≠ ∞) ⇒ μ(t) ≠ ∞$$

Lean4

theorem measure_ne_top_of_subset (h : t ⊆ s) (ht : μ s ≠ ∞) : μ t ≠ ∞ :=
  (measure_lt_top_of_subset h ht).ne

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

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

Разделы

Аффилиация

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