Theorems · Theorem · measure theory

MeasureTheory.inter_cylinder

∀ {ι : Type u_1} {α : ι → Type u_2} (s₁ s₂ : Finset ι) (S₁ : Set ((i : ↥s₁) → α ↑i)) (S₂ : Set ((i : ↥s₂) → α ↑i))
  [inst : DecidableEq ι],
  MeasureTheory.cylinder s₁ S₁ ∩ MeasureTheory.cylinder s₂ S₂ =
    MeasureTheory.cylinder (s₁ ∪ s₂) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∩ Finset.restrict₂ ⋯ ⁻¹' S₂)

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites7

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 and proof · cited by 13,712
Set.preimagestatement · cited by 4,946
Finset.subset_union_leftstatement · cited by 59
MeasureTheory.cylinderstatement · cited by 49
Finset.subset_union_rightstatement · cited by 45
Finset.restrict₂statement · cited by 44

Cited by2

Results whose statement or proof uses this declaration.

MeasureTheory.inter_mem_measurableCylindersproof · cited by 3
MeasureTheory.IsProjectiveMeasureFamily.congr_cylinderproof · cited by 1