English
The map a ↦ ⟨memPartitionSet t n a, memPartitionSet_mem t n a⟩ is measurable from countablePartition t n into the partition filtration.
Русский
Отображение a ↦ ⟨memPartitionSet t n a, memPartitionSet_mem t n a⟩ измеримо относительно разрешения partitionFiltration ht n.
LaTeX
$$$$ @Measurable\ a \mapsto \langle memPartitionSet(t,n,a), memPartitionSet_mem(t,n,a) \rangle \;: \text{(memPartition t n)} \to \text{partitionFiltration ht n} $$$$
Lean4
theorem measurable_memPartitionSet_subtype (ht : ∀ n, MeasurableSet (t n)) (n : ℕ)
(m : MeasurableSpace (memPartition t n)) :
@Measurable α (memPartition t n) (partitionFiltration ht n) m
(fun a ↦ ⟨memPartitionSet t n a, memPartitionSet_mem t n a⟩) :=
by
refine @measurable_to_countable' (memPartition t n) α m _ (partitionFiltration ht n) _ (fun s ↦ ?_)
rcases s with ⟨s, hs⟩
suffices MeasurableSet[partitionFiltration ht n] {x | memPartitionSet t n x = s}
by
convert this
ext x
simp
simp_rw [memPartitionSet_eq_iff _ hs]
exact measurableSet_partitionFiltration_of_mem _ _ hs
