feat: IndepFun.symm of different domains

leanprover-community · Jan 4, 2024 · c8597f2 · c8597f2
1 parent 7c03101
commit c8597f2
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/Mathlib/Probability/Independence/Basic.lean b/Mathlib/Probability/Independence/Basic.lean
@@ -650,8 +650,8 @@ theorem indepFun_iff_map_prod_eq_prod_map_map {mβ : MeasurableSpace β} {mβ' :
     rw [(h₀ hs ht).1, (h₀ hs ht).2, h, Measure.prod_prod]
 
 @[symm]
-nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {f g : Ω → β} (hfg : IndepFun f g μ) :
-    IndepFun g f μ := hfg.symm
+nonrec theorem IndepFun.symm [MeasurableSpace β] [MeasurableSpace γ] {f : Ω → β} {g : Ω → γ}
+    (hfg : IndepFun f g μ) : IndepFun g f μ := hfg.symm
 #align probability_theory.indep_fun.symm ProbabilityTheory.IndepFun.symm
 
 theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {f g f' g' : Ω → β} (hfg : IndepFun f g μ)

diff --git a/Mathlib/Probability/Independence/Kernel.lean b/Mathlib/Probability/Independence/Kernel.lean
@@ -788,8 +788,8 @@ theorem indepFun_iff_indepSet_preimage {mβ : MeasurableSpace β} {mβ' : Measur
   · rwa [← indepSet_iff_measure_inter_eq_mul (hf hs) (hg ht) κ μ]
 
 @[symm]
-nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {f g : Ω → β} (hfg : IndepFun f g κ μ) :
-    IndepFun g f κ μ := hfg.symm
+nonrec theorem IndepFun.symm {α : Type*} [MeasurableSpace α] [MeasurableSpace β]
+    {f : Ω → α} {g : Ω → β} (hfg : IndepFun f g κ μ) : IndepFun g f κ μ := hfg.symm
 
 theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {f g f' g' : Ω → β} (hfg : IndepFun f g κ μ)
     (hf : ∀ᵐ a ∂μ, f =ᵐ[κ a] f') (hg : ∀ᵐ a ∂μ, g =ᵐ[κ a] g') :