diff_mem

Mathlib.MeasureTheory.SetAlgebra

URI: https://scilib.ai/kg/mathlib#MeasureTheory.IsSetAlgebra.diff_mem

← MathLib Explorer

English

An algebra of sets is closed under difference.

Русский

Алгебра множеств замкнута по разности.

LaTeX

$$$s \\setminus t \\in 𝒜$$$

Lean4

/-- An algebra of sets is closed by difference. -/
theorem diff_mem (h𝒜 : IsSetAlgebra 𝒜) (s_mem : s ∈ 𝒜) (t_mem : t ∈ 𝒜) : s \ t ∈ 𝒜 :=
  h𝒜.inter_mem s_mem (h𝒜.compl_mem t_mem)

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

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

Разделы

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

Аффилиация

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