α : Type ?u.17624
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.17643
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
⊢ (∀ (i : ι), IsOpen (s ∩ ↑(U i))) ↔ ∀ (i : ι), IsOpen (Subtype.val ⁻¹' s)
α : Type ?u.17624
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.17643
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
⊢ IsOpen s ↔ ∀ (i : ι), IsOpen (Subtype.val ⁻¹' s)
rw [isOpen_iff_inter_of_iSup_eq_top hU s]
α : Type ?u.17624
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.17643
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
i : ι
⊢ IsOpen (s ∩ ↑(U i)) ↔ IsOpen (Subtype.val ⁻¹' s)
α : Type ?u.17624
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.17643
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
⊢ (∀ (i : ι), IsOpen (s ∩ ↑(U i))) ↔ ∀ (i : ι), IsOpen (Subtype.val ⁻¹' s)
refine forall_congr' fun i => ?_
α : Type ?u.17624
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.17643
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
i : ι
⊢ IsOpen (s ∩ ↑(U i)) ↔ IsOpen (Subtype.val '' (Subtype.val ⁻¹' s))
α : Type ?u.17624
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.17643
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
i : ι
⊢ IsOpen (s ∩ ↑(U i)) ↔ IsOpen (Subtype.val ⁻¹' s)
rw [(U _).2.openEmbedding_subtype_val.open_iff_image_open]
α : Type ?u.17624
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.17643
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
i : ι
⊢ IsOpen (s ∩ ↑(U i)) ↔ IsOpen (s ∩ range Subtype.val)
α : Type ?u.17624
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.17643
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
i : ι
⊢ IsOpen (s ∩ ↑(U i)) ↔ IsOpen (Subtype.val '' (Subtype.val ⁻¹' s))
erw [Set.image_preimage_eq_inter_range]
no goals
α : Type ?u.17624
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.17643
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
i : ι
⊢ IsOpen (s ∩ ↑(U i)) ↔ IsOpen (s ∩ range Subtype.val)
rw [Subtype.range_coe, Opens.carrier_eq_coe]