ext_iff' — Mathlib

English

κ = η iff ∀ a, s, MeasurableSet s → κ a s = η a s.

Русский

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

LaTeX

$$$\\\\kappa = \\\\eta \\\\iff \\\\forall a \\\\forall s \\\\ (MeasurableSet s \\\\rightarrow \\\\kappa a s = \\\\eta a s)$$$

Lean4

theorem ext_iff' : κ = η ↔ ∀ a s, MeasurableSet s → κ a s = η a s := by simp_rw [Kernel.ext_iff, Measure.ext_iff]

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