IsMetric

Mathlib.MeasureTheory.Measure.Hausdorff

URI: https://scilib.ai/kg/mathlib#MeasureTheory.OuterMeasure.IsMetric

Lean4

/-- We say that an outer measure `μ` in an (e)metric space is *metric* if `μ (s ∪ t) = μ s + μ t`
for any two metric separated sets `s`, `t`. -/
def IsMetric (μ : OuterMeasure X) : Prop :=
  ∀ s t : Set X, Metric.AreSeparated s t → μ (s ∪ t) = μ s + μ t

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru