English
If cylinder I S equals cylinder J T with S,T measurable, then P I S = P J T.
Русский
Если цилиндр I S равен цилиндру J T при измеримых S,T, то P I S = P J T.
LaTeX
$$$\forall S,T\ (MeasurableSet S)\ (MeasurableSet T)\ (Eq (cylinder I S) (cylinder J T)) \Rightarrow P I S = P J T.$$$
Lean4
theorem congr_cylinder (hP : IsProjectiveMeasureFamily P) {S : Set (∀ i : I, α i)} {T : Set (∀ i : J, α i)}
(hS : MeasurableSet S) (hT : MeasurableSet T) (h_eq : cylinder I S = cylinder J T) : P I S = P J T := by
classical
let U := Finset.restrict₂ Finset.subset_union_left ⁻¹' S ∩ Finset.restrict₂ Finset.subset_union_right ⁻¹' T
suffices P (I ∪ J) U = P I S ∧ P (I ∪ J) U = P J T from this.1.symm.trans this.2
constructor
· have h_eq_union : cylinder I S = cylinder (I ∪ J) U := by rw [← inter_cylinder, h_eq, inter_self]
exact hP.congr_cylinder_of_subset hS h_eq_union.symm Finset.subset_union_left
· have h_eq_union : cylinder J T = cylinder (I ∪ J) U := by rw [← inter_cylinder, h_eq, inter_self]
exact hP.congr_cylinder_of_subset hT h_eq_union.symm Finset.subset_union_right
