ae_eq_set_compl_compl

Mathlib.MeasureTheory.OuterMeasure.AE

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

← MathLib Explorer

English

sᶜ =ᵐ tᶜ iff s =ᵐ t

Русский

Дополнения множеств равны почти повсюду тогда и только тогда, когда множества равны почти повсюду.

LaTeX

$$$s^{c} =ᵐ[\mu] t^{c} \iff s =ᵐ[\mu] t$$$

Lean4

@[simp]
theorem ae_eq_set_compl_compl {s t : Set α} : sᶜ =ᵐ[μ] tᶜ ↔ s =ᵐ[μ] t := by
  simp only [← measure_symmDiff_eq_zero_iff, compl_symmDiff_compl]

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

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

Разделы

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

Аффилиация

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