union_ae_eq_right

Mathlib.MeasureTheory.OuterMeasure.AE

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

← MathLib Explorer

English

s ∪ t =ᵐ t ↔ μ(s \ t) = 0

Русский

s ∪ t =ᵐ t тогда и только тогда, когда μ(s \ t) = 0

LaTeX

$$$ (s \cup t) =ᵐ[μ] t \iff μ(s \setminus t) = 0 $$$

Lean4

theorem union_ae_eq_right : (s ∪ t : Set α) =ᵐ[μ] t ↔ μ (s \ t) = 0 := by
  simp [eventuallyLE_antisymm_iff, ae_le_set, union_diff_right, diff_eq_empty.2 Set.subset_union_right]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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