dirac_caratheodory — Mathlib

English

For every a in the type α, the outer Carathéodory measurable sets associated to the Dirac outer measure are all subsets; i.e., every subset is Carathéodory-measurable with respect to dirac a.

Русский

Для любого a из α множества, Carathéодорова-мера внешняя, связанная с мёрой Дирака, является измеримым по Каратеодору для всех подмножеств; то есть любое подмножество является Carathéodory-измеримым по мере dirac a.

LaTeX

$$$(\mathrm{dirac}(a)).\\mathrm{caratheodory} = \\top$$$

Lean4

@[simp]
theorem dirac_caratheodory (a : α) : (dirac a).caratheodory = ⊤ :=
  top_unique fun s _ t => by
    by_cases ht : a ∈ t; swap; · simp [ht]
    by_cases hs : a ∈ s <;> simp [*]

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