iSup_apply — Mathlib

English

Let α be a type, β a family of types β i, and f i : α → β i. Then the supremum of the family at a equals the supremum over i of f i a.

Русский

Пусть α — тип, β — семейство типов β i, и f i : α → β i. Тогда верхняя грань семейства в точке a равна верхней грани по i: (iSup_i f_i)(a) = iSup_i (f_i(a)).

LaTeX

$$$\\displaystyle (\\big\\vee_{i} f_i)(a) = \\big\\vee_{i} (f_i(a))$$$

Lean4

@[simp]
theorem iSup_apply {α : Type*} {β : α → Type*} {ι : Sort*} [∀ i, SupSet (β i)] {f : ι → ∀ a, β a} {a : α} :
    (⨆ i, f i) a = ⨆ i, f i a := by
  rw [iSup, sSup_apply, iSup, iSup, ← image_eq_range (fun f : ∀ i, β i => f a) (range f), ← range_comp]; rfl

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