Theorems · Definition · measure theory

MeasureTheory.measurableCylinders.finset

{ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → MeasurableSpace (α i)] →
      {t : Set ((i : ι) → α i)} → t ∈ MeasureTheory.measurableCylinders α → Finset ι

A finset s such that t = cylinder s S. S is given by measurableCylinders.set.

Defined in: Mathlib.MeasureTheory.Constructions.Cylinders
Cited by: 3 results in Mathlib
Foundations: Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Finsetstatement · cited by 13,712
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.measurableCylindersstatement and proof · cited by 48

Cited by5

Results whose statement or proof uses this declaration.

MeasureTheory.projectiveFamilyFunproof · cited by 4
MeasureTheory.projectiveFamilyContent_ne_topproof · cited by 3
MeasureTheory.measurableCylinders.setstatement · cited by 3
MeasureTheory.measurableCylinders.eq_cylinderstatement · cited by 1
MeasureTheory.measurableCylinders.measurableSetstatement · cited by 1