English
Triple induction principle for AEEqFun: if p holds for mk f hf, mk f' hf', mk f'' hf'', then p holds for f,f',f''.
Русский
Принцип тройной индукции для AEEqFun: если p выполняется для mk f hf, mk f' hf', mk f'' hf'', то p выполняется для f,f',f''.
LaTeX
$$$\\forall f,f',f''\\,\\forall hf,hf',hf'',\\; p(\\mathrm{mk} f hf, \\mathrm{mk} f' hf', \\mathrm{mk} f'' hf'') \\Rightarrow p(f,f',f'')$$$
Lean4
@[elab_as_elim]
theorem induction_on₃ {α' β' : Type*} [MeasurableSpace α'] [TopologicalSpace β'] {μ' : Measure α'} {α'' β'' : Type*}
[MeasurableSpace α''] [TopologicalSpace β''] {μ'' : Measure α''} (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β')
(f'' : α'' →ₘ[μ''] β'') {p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → (α'' →ₘ[μ''] β'') → Prop}
(H : ∀ f hf f' hf' f'' hf'', p (mk f hf) (mk f' hf') (mk f'' hf'')) : p f f' f'' :=
induction_on f fun f hf => induction_on₂ f' f'' <| H f hf
