measure_lt_top_of_subset

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

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

English

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

Русский

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

LaTeX

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

Lean4

theorem measure_lt_top_of_subset (hst : t ⊆ s) (hs : μ s ≠ ∞) : μ t < ∞ :=
  lt_of_le_of_lt (μ.mono hst) hs.lt_top

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

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

Разделы

Аффилиация

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