iUnion_Ioi_eq — Mathlib

English

If a is the GLB of s and a ∈ s, then the union over x ∈ s of the rays [x, ∞) is exactly the ray [a, ∞).

Русский

Если a — наименьшая нижняя граница множества s и a ∈ s, то объединение по x ∈ s лучей [x, ∞) равно лучу [a, ∞).

LaTeX

$$$$\bigcup_{x\in s} \mathrm{Ici}(x) = \mathrm{Ici}(a)$$$$

Lean4

theorem iUnion_Ioi_eq (h : IsGLB (range f) a) : ⋃ x, Ioi (f x) = Ioi a :=
  biUnion_range.symm.trans h.biUnion_Ioi_eq

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