iInf_apply — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem iInf_apply {α : Type*} {β : α → Type*} {ι : Sort*} [∀ i, InfSet (β i)] {f : ι → ∀ a, β a} {a : α} :
    (⨅ i, f i) a = ⨅ i, f i a :=
  @iSup_apply α (fun i => (β i)ᵒᵈ) _ _ _ _

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