ext_fun_iff — Mathlib

English

κ = η iff ∀ a f, Measurable f → ∫ f dκ a = ∫ f dη a.

Русский

κ = η тогда и только тогда, когда для всех a и для всех измеримых f выполняется ∫ f dκ a = ∫ f dη a.

LaTeX

$$$\\\\kappa = \\\\eta \\\\iff \\\\forall a \\\\forall f, \\\\text{Measurable } f \\rightarrow \\\\int f \\\\mathrm{d}\\\\kappa a = \\\\int f \\\\mathrm{d}\\\\eta a$$$

Lean4

theorem ext_fun_iff : κ = η ↔ ∀ a f, Measurable f → ∫⁻ b, f b ∂κ a = ∫⁻ b, f b ∂η a :=
  ⟨fun h a f _ => by rw [h], ext_fun⟩

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