English
The family of sets measurable with respect to μ.outerMeasure.caratheodory obeys the Carathéodory criterion: a set A is measurable iff for all open U, μ(U ∩ A) + μ(U \\ A) ≤ μ(U).
Русский
Множества, измеримые относительно μ.outerMeasure.caratheodory, удовлетворяют каратемодориному условию: A измеримо тогда и только тогда, когда для всех открытых U выполняется μ(U ∩ A) + μ(U \\ A) ≤ μ(U).
LaTeX
$$$$\\text{MeasurableSet}[μ.outerMeasure.caratheodory](A) \\iff \\forall U \\in \\mathrm{Opens}(G),\\ μ.outerMeasure(U \\cap A) + μ.outerMeasure(U \\setminus A) \\le μ.outerMeasure(U).$$$$
Lean4
theorem outerMeasure_caratheodory (A : Set G) :
MeasurableSet[μ.outerMeasure.caratheodory] A ↔
∀ U : Opens G, μ.outerMeasure (U ∩ A) + μ.outerMeasure (U \ A) ≤ μ.outerMeasure U :=
by
rw [Opens.forall]
apply inducedOuterMeasure_caratheodory
· apply innerContent_iUnion_nat
· apply innerContent_mono'
