α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
⊢ (∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)) → IsClosedMap f
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
⊢ IsClosedMap f ↔ ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
refine' ⟨fun h i => Set.restrictPreimage_isClosedMap _ h, _⟩
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
⊢ IsClosed (f '' s)
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
⊢ (∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)) → IsClosedMap f
rintro H s hs
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
⊢ ∀ (i : ι), IsClosed (Subtype.val ⁻¹' (f '' s))
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
⊢ IsClosed (f '' s)
rw [isClosed_iff_coe_preimage_of_iSup_eq_top hU]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
i : ι
⊢ IsClosed (Subtype.val ⁻¹' (f '' s))
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
⊢ ∀ (i : ι), IsClosed (Subtype.val ⁻¹' (f '' s))
intro i
case h.e'_3.h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
i : ι
e_1✝ : { x // x ∈ U i } = ↑(U i).carrier
⊢ Subtype.val ⁻¹' (f '' s) = restrictPreimage (U i).carrier f '' (Subtype.val ⁻¹' sᶜ)ᶜ
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
i : ι
⊢ IsClosed (Subtype.val ⁻¹' (f '' s))
convert H i _ ⟨⟨_, hs.1, eq_compl_comm.mpr rfl⟩⟩
case h.e'_3.h.h.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
i : ι
e_1✝ : { x // x ∈ U i } = ↑(U i).carrier
x : β
hx : x ∈ U i
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' (f '' s) ↔
    { val := x, property := hx } ∈ restrictPreimage (U i).carrier f '' (Subtype.val ⁻¹' sᶜ)ᶜ
case h.e'_3.h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
i : ι
e_1✝ : { x // x ∈ U i } = ↑(U i).carrier
⊢ Subtype.val ⁻¹' (f '' s) = restrictPreimage (U i).carrier f '' (Subtype.val ⁻¹' sᶜ)ᶜ
ext ⟨x, hx⟩
case h.e'_3.h.h.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
i : ι
e_1✝ : { x // x ∈ U i } = ↑(U i).carrier
x : β
hx : x ∈ U i
⊢ (∃ y, y ∈ s ∧ f y = x) ↔ ∃ y, y ∈ s ∧ f y ∈ U i ∧ f y = x
case h.e'_3.h.h.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
i : ι
e_1✝ : { x // x ∈ U i } = ↑(U i).carrier
x : β
hx : x ∈ U i
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' (f '' s) ↔
    { val := x, property := hx } ∈ restrictPreimage (U i).carrier f '' (Subtype.val ⁻¹' sᶜ)ᶜ
suffices (∃ y, y ∈ s ∧ f y = x) ↔ ∃ y, y ∈ s ∧ f y ∈ U i ∧ f y = x by
  simpa [Set.restrictPreimage, ← Subtype.coe_inj]
no goals
case h.e'_3.h.h.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
i : ι
e_1✝ : { x // x ∈ U i } = ↑(U i).carrier
x : β
hx : x ∈ U i
⊢ (∃ y, y ∈ s ∧ f y = x) ↔ ∃ y, y ∈ s ∧ f y ∈ U i ∧ f y = x
exact ⟨fun ⟨a, b, c⟩ => ⟨a, b, c.symm ▸ hx, c⟩, fun ⟨a, b, _, c⟩ => ⟨a, b, c⟩⟩
no goals
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.21339
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
i : ι
e_1✝ : { x // x ∈ U i } = ↑(U i).carrier
x : β
hx : x ∈ U i
this : (∃ y, y ∈ s ∧ f y = x) ↔ ∃ y, y ∈ s ∧ f y ∈ U i ∧ f y = x
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' (f '' s) ↔
    { val := x, property := hx } ∈ restrictPreimage (U i).carrier f '' (Subtype.val ⁻¹' sᶜ)ᶜ
simpa [Set.restrictPreimage, ← Subtype.coe_inj]