no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
s : Set α
I : Set β
S : β → Set α
H : Set.Finite I
⊢ BddAbove (⋃ (i : β) (_ : i ∈ ∅), S i) ↔ ∀ (i : β), i ∈ ∅ → BddAbove (S i)
simp only [biUnion_empty, bddAbove_empty, ball_empty_iff]
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
s : Set α
I : Set β
S : β → Set α
H : Set.Finite I
a✝ : β
s✝ : Set β
x✝¹ : ¬a✝ ∈ s✝
x✝ : Set.Finite s✝
hs : BddAbove (⋃ (i : β) (_ : i ∈ s✝), S i) ↔ ∀ (i : β), i ∈ s✝ → BddAbove (S i)
⊢ BddAbove (⋃ (i : β) (_ : i ∈ insert a✝ s✝), S i) ↔ ∀ (i : β), i ∈ insert a✝ s✝ → BddAbove (S i)
simp only [biUnion_insert, ball_insert_iff, bddAbove_union, hs]