English
Let f be antitone and g be monotone, with a being a GLB of the range of f and b an LUB of the range of g. Then the union over x of Ioo(f(x), g(x)) equals Ioo(a, b).
Русский
Пусть f антитонна, g монотонна; пусть a — наименьшая верхняя граница множества значений f, b — наименьшая верхняя граница значений g. Тогда объединение по x множества Ioo(f(x), g(x)) равно Ioo(a, b).
LaTeX
$$$\bigcup_{x} \mathrm{Ioo}(f(x), g(x)) = \mathrm{Ioo}(a, b) \quad \text{при } \mathrm{IsGLB}(\mathrm{range}(f), a) \text{ и } \mathrm{IsLUB}(\mathrm{range}(g), b).$$$
Lean4
theorem iUnion_Ioo_of_mono_of_isGLB_of_isLUB (hf : Antitone f) (hg : Monotone g) (ha : IsGLB (range f) a)
(hb : IsLUB (range g) b) : ⋃ x, Ioo (f x) (g x) = Ioo a b :=
calc
⋃ x, Ioo (f x) (g x) = (⋃ x, Ioi (f x)) ∩ ⋃ x, Iio (g x) := iUnion_inter_of_monotone hf.Ioi hg.Iio
_ = Ioi a ∩ Iio b := congr_arg₂ (· ∩ ·) ha.iUnion_Ioi_eq hb.iUnion_Iio_eq
