pos_mono

Mathlib.MeasureTheory.OuterMeasure.Basic

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

English

If s ⊆ t and 0 < μ s, then 0 < μ t.

Русский

Если s ⊆ t и 0 < μ s, то 0 < μ t.

LaTeX

$$$(s \subseteq t) \land (0 < \mu s) \Rightarrow 0 < \mu t$$$

Lean4

theorem pos_mono ⦃s t : Set α⦄ (h : s ⊆ t) (hs : 0 < μ s) : 0 < μ t :=
  hs.trans_le <| measure_mono h

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

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

Разделы

Аффилиация

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