Theorems · Definition · measure theory

MeasureTheory.cylinder

{ι : Type u_1} → {α : ι → Type u_2} → (s : Finset ι) → Set ((i : ↥s) → α ↑i) → Set ((i : ι) → α i)

Given a finite set s of indices, a cylinder is the preimage of a set S of ∀ i : s, α i by the projection from ∀ i, α i to ∀ i : s, α i.

Defined in

Mathlib.MeasureTheory.Constructions.Cylinders

Cited by

49 results in Mathlib

Foundations

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