ciInf_subtype' — Mathlib

English

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

Русский

Пусть непусто ι, p: ι → Prop, и f: ∀ i, p i → α. Тогда инфиму́м по i, h равен инфиму́му по подтипу.

LaTeX

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

Lean4

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

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