case inl
α : Type u_1
β : Type u_2
ι : Type ?u.2500
π : ι → Type ?u.2505
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
t : Set β
S : (i : ι) → Set (π i)
⊢ IsBounded (∅ ×ˢ t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsBounded ∅ ∧ IsBounded t

case inr
α : Type u_1
β : Type u_2
ι : Type ?u.2500
π : ι → Type ?u.2505
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hs : Set.Nonempty s
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
α : Type u_1
β : Type u_2
ι : Type ?u.2500
π : ι → Type ?u.2505
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
rcases s.eq_empty_or_nonempty with (rfl | hs)
case inr.inl
α : Type u_1
β : Type u_2
ι : Type ?u.2500
π : ι → Type ?u.2505
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
S : (i : ι) → Set (π i)
hs : Set.Nonempty s
⊢ IsBounded (s ×ˢ ∅) ↔ s = ∅ ∨ ∅ = ∅ ∨ IsBounded s ∧ IsBounded ∅

case inr.inr
α : Type u_1
β : Type u_2
ι : Type ?u.2500
π : ι → Type ?u.2505
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
case inr
α : Type u_1
β : Type u_2
ι : Type ?u.2500
π : ι → Type ?u.2505
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hs : Set.Nonempty s
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
rcases t.eq_empty_or_nonempty with (rfl | ht)
no goals
case inr.inr
α : Type u_1
β : Type u_2
ι : Type ?u.2500
π : ι → Type ?u.2505
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
simp only [hs.ne_empty, ht.ne_empty, isBounded_prod_of_nonempty (hs.prod ht), false_or_iff]
no goals
case inl
α : Type u_1
β : Type u_2
ι : Type ?u.2500
π : ι → Type ?u.2505
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
t : Set β
S : (i : ι) → Set (π i)
⊢ IsBounded (∅ ×ˢ t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsBounded ∅ ∧ IsBounded t
simp
no goals
case inr.inl
α : Type u_1
β : Type u_2
ι : Type ?u.2500
π : ι → Type ?u.2505
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
S : (i : ι) → Set (π i)
hs : Set.Nonempty s
⊢ IsBounded (s ×ˢ ∅) ↔ s = ∅ ∨ ∅ = ∅ ∨ IsBounded s ∧ IsBounded ∅
simp