ciSup_subtype' — Mathlib

English

Let Nonempty ι and p: ι → Prop, and f: ∀ i, p i → α. The supremum over i and h with h : p i of f(i,h) equals the supremum over x : Subtype p of f(x).

Русский

Пусть непусто ι, p: ι → Prop, и f: ∀ i, p i → α. Тогда sup { f(i,h) } равен sup { f(x) : x ∈ Subtype p }.

LaTeX

$$$\sup_{i} \sup_{h: p(i)} f(i,h) = \sup_{x: \mathrm{Subtype}(p)} f(x).$$$

Lean4

theorem ciSup_subtype' [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : ∀ i, p i → α}
    (hf : BddAbove (Set.range (fun i : Subtype p ↦ f i i.prop))) (hf' : sSup ∅ ≤ ⨆ (i : Subtype p), f i i.prop) :
    ⨆ (i) (h), f i h = ⨆ x : Subtype p, f x x.property :=
  (ciSup_subtype (f := fun x => f x.val x.property) hf hf').symm

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