[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
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
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hs)
[GOAL]
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
t : Set β
S : (i : ι) → Set (π i)
⊢ IsBounded (∅ ×ˢ t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsBounded ∅ ∧ IsBounded t
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
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
[PROOFSTEP]
rcases t.eq_empty_or_nonempty with (rfl | ht)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
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 ∅
[PROOFSTEP]
simp
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
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
[PROOFSTEP]
simp only [hs.ne_empty, ht.ne_empty, isBounded_prod_of_nonempty (hs.prod ht), false_or_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
s : Set α
t : Set β
S : (i : ι) → Set (π i)
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hs)
[GOAL]
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
t : Set β
S : (i : ι) → Set (π i)
⊢ IsBounded (∅ ×ˢ ∅) ↔ IsBounded ∅
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
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
[PROOFSTEP]
exact (isBounded_prod_of_nonempty (hs.prod hs)).trans (and_self_iff _)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
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)
[PROOFSTEP]
by_cases hne : ∃ i, S i = ∅
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
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)
[PROOFSTEP]
simp [hne, univ_pi_eq_empty_iff.2 hne]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
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)
[PROOFSTEP]
simp only [hne, false_or_iff]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
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)
[PROOFSTEP]
simp only [not_exists, ← Ne.def, ← nonempty_iff_ne_empty, ← univ_pi_nonempty_iff] at hne 
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
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)
[PROOFSTEP]
exact isBounded_pi_of_nonempty hne
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Bornology α
inst✝³ : Bornology β
inst✝² : (i : ι) → Bornology (π i)
inst✝¹ : BoundedSpace α
inst✝ : BoundedSpace β
⊢ BoundedSpace (α × β)
[PROOFSTEP]
simp [← cobounded_eq_bot_iff, cobounded_prod]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Bornology α
inst✝² : Bornology β
inst✝¹ : (i : ι) → Bornology (π i)
inst✝ : ∀ (i : ι), BoundedSpace (π i)
⊢ BoundedSpace ((i : ι) → π i)
[PROOFSTEP]
simp [← cobounded_eq_bot_iff, cobounded_pi]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Bornology α✝
inst✝² : Bornology β✝
inst✝¹ : (i : ι) → Bornology (π i)
α : Type u_5
β : Type u_6
inst✝ : Bornology β
f : α → β
⊢ BoundedSpace α ↔ IsBounded (range f)
[PROOFSTEP]
rw [← @isBounded_univ _ (Bornology.induced f), isBounded_induced, image_univ]
  -- porting note: had to explicitly provided the bornology to `isBounded_univ`.
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
p : α → Prop
⊢ BoundedSpace (Subtype p) ↔ IsBounded {x | p x}
[PROOFSTEP]
rw [boundedSpace_induced_iff, Subtype.range_coe_subtype]
