Theorems · Theorem · measure theory

MeasureTheory.IsSetAlgebra.biInter_mem

∀ {α : Type u_1} {𝒜 : Set (Set α)} {ι : Type u_2},
  MeasureTheory.IsSetAlgebra 𝒜 → ∀ {s : ι → Set α} (S : Finset ι), (∀ i ∈ S, s i ∈ 𝒜) → ⋂ i ∈ S, s i ∈ 𝒜

An algebra of sets is closed by finite intersections.

Defined in

Mathlib.MeasureTheory.SetAlgebra

Cited by

0 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound