isGLB_iUnion_iff_of_isLUB — Mathlib

English

Let u : ι → α with IsGLB(s_i, u_i) for all i. Then for any c ∈ α, IsGLB(Set.range u, c) holds iff IsGLB(⋃_i s_i, c).

Русский

Пусть u : ι → α и для каждого i выполняется IsGLB (s_i, u_i). Тогда для любого c: IsGLB(Set.range u, c) эквивалентно IsGLB(⋃_i s_i, c).

LaTeX

$$$\\left( \\forall i, \\IsGLB(s_i, u_i) \\right) \\to \\left( \\IsGLB(\\operatorname{Range}(u), c) \\iff \\IsGLB\\left(\\bigcup_i s_i\\right, c) \\right).$$$

Lean4

theorem isGLB_iUnion_iff_of_isLUB {u : ι → α} (hs : ∀ i, IsGLB (s i) (u i)) (c : α) :
    IsGLB (Set.range u) c ↔ IsGLB (⋃ i, s i) c :=
  by
  refine isGLB_congr ?_
  simp_rw [range_eq_iUnion, lowerBounds_iUnion, lowerBounds_singleton, (hs _).lowerBounds_eq]

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