ae_le_set_inter

Mathlib.MeasureTheory.OuterMeasure.AE

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

English

If s ≤ᵐ t and s' ≤ᵐ t', then (s ∩ s') ≤ᵐ (t ∩ t').

Русский

Если s ≤ᵐ t и s' ≤ᵐ t', то (s ∩ s') ≤ᵐ (t ∩ t').

LaTeX

$$$(s \leq_{\mathrm{a.e.}} t) \Rightarrow (s' \leq_{\mathrm{a.e.}} t') \Rightarrow (s \cap s') \leq_{\mathrm{a.e.}} (t \cap t')$$$

Lean4

theorem ae_le_set_inter {s' t' : Set α} (h : s ≤ᵐ[μ] t) (h' : s' ≤ᵐ[μ] t') : (s ∩ s' : Set α) ≤ᵐ[μ] (t ∩ t' : Set α) :=
  h.inter h'

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

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

Разделы

Аффилиация

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