isSetRing

Mathlib.MeasureTheory.SetAlgebra

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

← MathLib Explorer

English

An algebra of sets is a ring of sets.

Русский

Алгебра множеств является кольцом множеств.

LaTeX

$$$\\text{IsSetAlgebra } 𝒜 \\Rightarrow \\text{IsSetRing } 𝒜$$$

Lean4

/-- An algebra of sets is a ring of sets. -/
theorem isSetRing (h𝒜 : IsSetAlgebra 𝒜) : IsSetRing 𝒜
    where
  empty_mem := h𝒜.empty_mem
  union_mem := h𝒜.union_mem
  diff_mem := fun _ _ ↦ h𝒜.diff_mem

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

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

Разделы

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

Аффилиация

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