cbiSup_eq_of_forall — Mathlib

English

Let hp: ∀ i, p(i). Then the supremum over i of the inner supremums equals the supremum of f over the entire Subtype p.

Русский

Пусть выполнено ∀ i, p(i). Тогда верхняя грань по i и внутренних гранумов равна верхней грани по f на [Subtype p].

LaTeX

$$hp : ∀ i, p i → ⨆ i (h : p i), f ⟨i, h⟩ = iSup f$$

Lean4

theorem cbiSup_eq_of_forall {p : ι → Prop} {f : Subtype p → α} (hp : ∀ i, p i) : ⨆ (i) (h : p i), f ⟨i, h⟩ = iSup f :=
  by
  simp only [hp, ciSup_unique]
  simp only [iSup]
  congr
  apply Subset.antisymm
  · rintro - ⟨i, rfl⟩
    simp
  · rintro - ⟨i, rfl⟩
    simp

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