English
Let Nonempty ι and p: ι → Prop with [Nonempty (Subtype p)]. For f : Subtype p → α, the supremum over i ∈ ι of f i (where i ranges with a witness h ∈ p i) equals the supremum over x ∈ Subtype p of f x.
Русский
Пусть непусто ι и p: ι → Prop, существует непустой подтип. Для f: Subtype p → α равенство: верхняя граница по всем i ∈ ι равна верхней границе по всей подтиповой функции.
LaTeX
$$$\sup_{i: ι} f(i) = \sup_{x: \mathrm{Subtype}(p)} f(x) \quad\text{where } f(i) = f(\langle i, - \rangle)$.$$
Lean4
theorem ciSup_subtype [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : Subtype p → α}
(hf : BddAbove (Set.range f)) (hf' : sSup ∅ ≤ iSup f) : iSup f = ⨆ (i) (h : p i), f ⟨i, h⟩ := by
classical
refine le_antisymm (ciSup_le ?_) ?_
· intro ⟨i, h⟩
have : f ⟨i, h⟩ = (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩) i := by simp [h]
rw [this]
refine le_ciSup (f := (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩)) ?_ i
simp_rw [ciSup_eq_ite]
refine (hf.union (bddAbove_singleton (a := sSup ∅))).mono ?_
intro
simp only [Set.mem_range, Set.union_singleton, Set.mem_insert_iff, Subtype.exists, forall_exists_index]
intro b hb
split_ifs at hb
· exact Or.inr ⟨_, _, hb⟩
· simp_all
· refine ciSup_le fun i ↦ ?_
simp_rw [ciSup_eq_ite]
split_ifs
· exact le_ciSup hf ?_
· exact hf'
