iSup_sInfGen_nonempty — Mathlib

English

If m is nonempty, then the supremum over nonempty t of sInfGen m t equals the infimum over μ ∈ m of μ(t).

Русский

Если m непусто, то наибольший верхний предел над не пустыми t даёт инфимуум по μ ∈ m от μ(t).

LaTeX

$$$\\big\\lVert\\,\\!\\!\\!\\!\\! \\; \\big\\rVert_{t.Nonempty} sInfGen\\, m\\, t = \\inf_{\\mu \\in m} \\mu(t)$$$

Lean4

theorem iSup_sInfGen_nonempty {m : Set (OuterMeasure α)} (h : m.Nonempty) (t : Set α) :
    ⨆ _ : t.Nonempty, sInfGen m t = ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), μ t :=
  by
  rcases t.eq_empty_or_nonempty with (rfl | ht)
  · simp [biInf_const h]
  · simp [ht, sInfGen_def]

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