case mp
α : Type ?u.13206
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.13225
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
⊢ IsOpen s → ∀ (i : ι), IsOpen (s ∩ ↑(U i))

case mpr
α : Type ?u.13206
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.13225
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
⊢ (∀ (i : ι), IsOpen (s ∩ ↑(U i))) → IsOpen s
α : Type ?u.13206
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.13225
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
⊢ IsOpen s ↔ ∀ (i : ι), IsOpen (s ∩ ↑(U i))
constructor
no goals
case mp
α : Type ?u.13206
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.13225
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
⊢ IsOpen s → ∀ (i : ι), IsOpen (s ∩ ↑(U i))
exact fun H i => H.inter (U i).2
case mpr
α : Type ?u.13206
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.13225
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
⊢ IsOpen s
case mpr
α : Type ?u.13206
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.13225
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
⊢ (∀ (i : ι), IsOpen (s ∩ ↑(U i))) → IsOpen s
intro H
case mpr
α : Type ?u.13206
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.13225
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
this : (⋃ (i : ι), ↑(U i)) = univ
⊢ IsOpen s
case mpr
α : Type ?u.13206
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.13225
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
⊢ IsOpen s
have : (⋃ i, (U i : Set β)) = Set.univ := by
  convert congr_arg (SetLike.coe) hU
  simp
case mpr
α : Type ?u.13206
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.13225
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
this : (⋃ (i : ι), ↑(U i)) = univ
⊢ IsOpen (⋃ (i : ι), s ∩ ↑(U i))
case mpr
α : Type ?u.13206
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.13225
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
this : (⋃ (i : ι), ↑(U i)) = univ
⊢ IsOpen s
rw [← s.inter_univ, ← this, Set.inter_iUnion]
no goals
case mpr
α : Type ?u.13206
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.13225
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
this : (⋃ (i : ι), ↑(U i)) = univ
⊢ IsOpen (⋃ (i : ι), s ∩ ↑(U i))
exact isOpen_iUnion H
case h.e'_2
α : Type ?u.13206
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.13225
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
⊢ (⋃ (i : ι), ↑(U i)) = ↑(iSup U)
α : Type ?u.13206
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.13225
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
⊢ (⋃ (i : ι), ↑(U i)) = univ
convert congr_arg (SetLike.coe) hU
no goals
case h.e'_2
α : Type ?u.13206
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.13225
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
⊢ (⋃ (i : ι), ↑(U i)) = ↑(iSup U)
simp