induction_on₂ — Mathlib

English

If a property holds for mk f hf and mk f' hf', then it holds for f and f' simultaneously.

Русский

Если свойство выполняется для mk f hf и mk f' hf', то для f и f' одновременно оно выполняется.

LaTeX

$$$\\forall f,f'\\,\\forall hf, hf',\\; p(\\mathrm{mk} f hf, \\mathrm{mk} f' hf') \\Rightarrow p(f,f')$$$

Lean4

@[elab_as_elim]
theorem induction_on₂ {α' β' : Type*} [MeasurableSpace α'] [TopologicalSpace β'] {μ' : Measure α'} (f : α →ₘ[μ] β)
    (f' : α' →ₘ[μ'] β') {p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → Prop} (H : ∀ f hf f' hf', p (mk f hf) (mk f' hf')) :
    p f f' :=
  induction_on f fun f hf => induction_on f' <| H f hf

Похожие утверждения