case inl
α : Type u_1
β : Type ?u.3457
ι : Type ?u.3460
π : ι → Type ?u.3465
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
t : Set β
S : (i : ι) → Set (π i)
⊢ IsBounded (∅ ×ˢ ∅) ↔ IsBounded ∅

case inr
α : Type u_1
β : Type ?u.3457
ι : Type ?u.3460
π : ι → Type ?u.3465
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hs : Set.Nonempty s
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s
α : Type u_1
β : Type ?u.3457
ι : Type ?u.3460
π : ι → Type ?u.3465
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s
rcases s.eq_empty_or_nonempty with (rfl | hs)
no goals
case inr
α : Type u_1
β : Type ?u.3457
ι : Type ?u.3460
π : ι → Type ?u.3465
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hs : Set.Nonempty s
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s
exact (isBounded_prod_of_nonempty (hs.prod hs)).trans (and_self_iff _)
no goals
case inl
α : Type u_1
β : Type ?u.3457
ι : Type ?u.3460
π : ι → Type ?u.3465
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
t : Set β
S : (i : ι) → Set (π i)
⊢ IsBounded (∅ ×ˢ ∅) ↔ IsBounded ∅
simp