mono''

Mathlib.MeasureTheory.OuterMeasure.Operations

URI: https://scilib.ai/kg/mathlib#MeasureTheory.OuterMeasure.mono''

English

If m1 ≤ m2 and s1 ⊆ s2, then m1(s1) ≤ m2(s2).

Русский

Если m1 ≤ m2 и s1 ⊆ s2, то m1(s1) ≤ m2(s2).

LaTeX

$$$ m_1 \le m_2 \quad \&\&\quad s_1 \subseteq s_2 \Rightarrow m_1(s_1) \le m_2(s_2) $$$

Lean4

@[mono, gcongr]
theorem mono'' {m₁ m₂ : OuterMeasure α} {s₁ s₂ : Set α} (hm : m₁ ≤ m₂) (hs : s₁ ⊆ s₂) : m₁ s₁ ≤ m₂ s₂ :=
  (hm s₁).trans (m₂.mono hs)

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

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

Разделы

Аффилиация

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