Theorems · Theorem · measure theory

MeasureTheory.SimpleFunc.pair_preimage

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β)
  (g : MeasureTheory.SimpleFunc α γ) (s : Set β) (t : Set γ), ⇑(f.pair g) ⁻¹' s ×ˢ t = ⇑f ⁻¹' s ∩ ⇑g ⁻¹' t

Defined in

Mathlib.MeasureTheory.Function.SimpleFunc

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace