case pos
α : Type ?u.78124
β : Type ?u.78127
ι : Type u_2
π : ι → Type u_1
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hne : ∃ i, S i = ∅
⊢ IsBounded (Set.pi univ S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)

case neg
α : Type ?u.78124
β : Type ?u.78127
ι : Type u_2
π : ι → Type u_1
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hne : ¬∃ i, S i = ∅
⊢ IsBounded (Set.pi univ S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
α : Type ?u.78124
β : Type ?u.78127
ι : Type u_2
π : ι → Type u_1
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
⊢ IsBounded (Set.pi univ S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
by_cases hne : ∃ i, S i = ∅
no goals
case pos
α : Type ?u.78124
β : Type ?u.78127
ι : Type u_2
π : ι → Type u_1
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hne : ∃ i, S i = ∅
⊢ IsBounded (Set.pi univ S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
simp [hne, univ_pi_eq_empty_iff.2 hne]
case neg
α : Type ?u.78124
β : Type ?u.78127
ι : Type u_2
π : ι → Type u_1
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hne : ¬∃ i, S i = ∅
⊢ IsBounded (Set.pi univ S) ↔ ∀ (i : ι), IsBounded (S i)
case neg
α : Type ?u.78124
β : Type ?u.78127
ι : Type u_2
π : ι → Type u_1
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hne : ¬∃ i, S i = ∅
⊢ IsBounded (Set.pi univ S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
simp only [hne, false_or_iff]
case neg
α : Type ?u.78124
β : Type ?u.78127
ι : Type u_2
π : ι → Type u_1
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hne : Set.Nonempty (Set.pi univ fun i => S i)
⊢ IsBounded (Set.pi univ S) ↔ ∀ (i : ι), IsBounded (S i)
case neg
α : Type ?u.78124
β : Type ?u.78127
ι : Type u_2
π : ι → Type u_1
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hne : ¬∃ i, S i = ∅
⊢ IsBounded (Set.pi univ S) ↔ ∀ (i : ι), IsBounded (S i)
simp only [not_exists, ← Ne.def, ← nonempty_iff_ne_empty, ← univ_pi_nonempty_iff] at hne
no goals
case neg
α : Type ?u.78124
β : Type ?u.78127
ι : Type u_2
π : ι → Type u_1
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hne : Set.Nonempty (Set.pi univ fun i => S i)
⊢ IsBounded (Set.pi univ S) ↔ ∀ (i : ι), IsBounded (S i)
exact isBounded_pi_of_nonempty hne