English
The germ of comp₂Measurable g hg f₁ f₂ equals the germ obtained from the two inputs via the function g with appropriate aemeasurable data.
Русский
Гарм comp₂Measurable равен гарму, полученному из двух входов через g с корректной aemeasurable-данной.
LaTeX
$$$(comp₂Measurable g hg f₁ f₂).toGerm = f₁.toGerm.map₂ g f₂.toGerm$$$
Lean4
theorem comp₂Measurable_toGerm [PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] [PseudoMetrizableSpace γ]
[SecondCountableTopologyEither β γ] [MeasurableSpace γ] [BorelSpace γ] [PseudoMetrizableSpace δ]
[SecondCountableTopology δ] [MeasurableSpace δ] [OpensMeasurableSpace δ] (g : β → γ → δ)
(hg : Measurable (uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
(comp₂Measurable g hg f₁ f₂).toGerm = f₁.toGerm.map₂ g f₂.toGerm :=
induction_on₂ f₁ f₂ fun f₁ _ f₂ _ => by simp
