case inl
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : s ×ˢ t = ∅
⊢ IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅

case inr
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
⊢ IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
⊢ IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
cases' (s ×ˢ t).eq_empty_or_nonempty with h h
no goals
case inl
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : s ×ˢ t = ∅
⊢ IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
simp [h, prod_eq_empty_iff.1 h]
case inr
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
⊢ IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
case inr
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
⊢ IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
have st : s.Nonempty ∧ t.Nonempty := prod_nonempty_iff.1 h
case inr.mp
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
⊢ IsOpen (s ×ˢ t) → IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅

case inr.mpr
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
⊢ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅ → IsOpen (s ×ˢ t)
case inr
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
⊢ IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
constructor
case inr.mp
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
case inr.mp
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
⊢ IsOpen (s ×ˢ t) → IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
intro (H : IsOpen (s ×ˢ t))
case inr.mp.refine'_1
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen s

case inr.mp.refine'_2
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen t
case inr.mp
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
refine' Or.inl ⟨_, _⟩
case inr.mp.refine'_1
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen s

case inr.mp.refine'_2
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen t
case inr.mp.refine'_1
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen s

case inr.mp.refine'_2
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen t
show IsOpen s
case inr.mp.refine'_2
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen t
case inr.mp.refine'_2
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen t
show IsOpen t
case inr.mp.refine'_1
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen (Prod.fst '' s ×ˢ t)
case inr.mp.refine'_1
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen s
rw [← fst_image_prod s st.2]
no goals
case inr.mp.refine'_1
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen (Prod.fst '' s ×ˢ t)
exact isOpenMap_fst _ H
case inr.mp.refine'_2
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen (Prod.snd '' s ×ˢ t)
case inr.mp.refine'_2
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen t
rw [← snd_image_prod st.1 t]
no goals
case inr.mp.refine'_2
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen (s ×ˢ t)
⊢ IsOpen (Prod.snd '' s ×ˢ t)
exact isOpenMap_snd _ H
case inr.mpr
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
⊢ IsOpen (s ×ˢ t)
case inr.mpr
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
⊢ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅ → IsOpen (s ×ˢ t)
intro H
case inr.mpr
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen s ∧ IsOpen t
⊢ IsOpen (s ×ˢ t)
case inr.mpr
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
⊢ IsOpen (s ×ˢ t)
simp only [st.1.ne_empty, st.2.ne_empty, not_false_iff, or_false_iff] at H
no goals
case inr.mpr
α : Type u
β : Type v
γ : Type ?u.57822
δ : Type ?u.57825
ε : Type ?u.57828
ζ : Type ?u.57831
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : IsOpen s ∧ IsOpen t
⊢ IsOpen (s ×ˢ t)
exact H.1.prod H.2