sInfGen_def

Mathlib.MeasureTheory.OuterMeasure.OfFunction

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

English

sInfGen m s equals the infimum of μ(s) over μ ∈ m.

Русский

sInfGen m s равен инфимууму по μ(s) для μ ∈ m.

LaTeX

$$$ sInfGen\\, m\\, s = \\inf_{\\mu \\in m} \\mu(s) $$$

Lean4

theorem sInfGen_def (m : Set (OuterMeasure α)) (t : Set α) : sInfGen m t = ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), μ t :=
  rfl

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

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

Разделы

Аффилиация

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