Theorems · Definition · measure theory

MeasureTheory.squareCylinders

{ι : Type u_1} → {α : ι → Type u_2} → ((i : ι) → Set (Set (α i))) → Set (Set ((i : ι) → α i))

Given a finite set s of indices, a square cylinder is the product of a set S of ∀ i : s, α i and of univ on the other indices. The set S is a product of sets t i such that for all i : s, t i ∈ C i. squareCylinders is the set of all such square cylinders.

Defined in

Mathlib.MeasureTheory.Constructions.Cylinders

Cited by

6 results in Mathlib

Foundations

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