ciInf_subtype — Mathlib

English

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

Русский

Пусть непусто ι и p: ι → Prop, существует непустой подтип. Для f: Subtype p → α инфиму́м по всем i равен инфиму́му по подтипу.

LaTeX

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

Lean4

theorem ciInf_subtype [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : Subtype p → α}
    (hf : BddBelow (Set.range f)) (hf' : iInf f ≤ sInf ∅) : iInf f = ⨅ (i) (h : p i), f ⟨i, h⟩ :=
  ciSup_subtype (α := αᵒᵈ) hf hf'

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