Ici_ciSup — Mathlib

English

Let Nonempty ι and f: ι → α with range bounded above. Then Ici( sup_i f(i) ) equals ⋂ i, Ici(f(i)).

Русский

Пусть непусто ι и f: ι → α с верхней гранью. Тогда Ici( sup_i f(i) ) равняется ⋂ i, Ici(f(i)).

LaTeX

$$$\mathrm{Ici}\Big(\sup_{i} f(i)\Big) = \bigcap_{i} \mathrm{Ici}(f(i)).$$$

Lean4

theorem Ici_ciSup [Nonempty ι] {f : ι → α} (hf : BddAbove (range f)) : Ici (⨆ i, f i) = ⋂ i, Ici (f i) :=
  Iic_ciInf (α := αᵒᵈ) hf

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