[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
h : Inducing f
⊢ Inducing (restrictPreimage s f)
[PROOFSTEP]
simp_rw [inducing_subtype_val.inducing_iff, inducing_iff_nhds, restrictPreimage, MapsTo.coe_restrict, restrict_eq, ←
  @Filter.comap_comap _ _ _ _ _ f, Function.comp_apply] at h ⊢
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
h : ∀ (a : α), 𝓝 a = comap f (𝓝 (f a))
⊢ ∀ (a : ↑(f ⁻¹' s)), 𝓝 a = comap Subtype.val (comap f (𝓝 (f ↑a)))
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
h : ∀ (a : α), 𝓝 a = comap f (𝓝 (f a))
a : ↑(f ⁻¹' s)
⊢ 𝓝 a = comap Subtype.val (comap f (𝓝 (f ↑a)))
[PROOFSTEP]
rw [← h, ← inducing_subtype_val.nhds_eq_comap]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : IsClosedMap f
⊢ IsClosedMap (restrictPreimage s f)
[PROOFSTEP]
rintro t ⟨u, hu, e⟩
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : IsClosedMap f
t : Set ↑(f ⁻¹' s)
u : Set α
hu : IsOpen u
e : Subtype.val ⁻¹' u = tᶜ
⊢ IsClosed (restrictPreimage s f '' t)
[PROOFSTEP]
refine' ⟨⟨_, (H _ (IsOpen.isClosed_compl hu)).1, _⟩⟩
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : IsClosedMap f
t : Set ↑(f ⁻¹' s)
u : Set α
hu : IsOpen u
e : Subtype.val ⁻¹' u = tᶜ
⊢ Subtype.val ⁻¹' (f '' uᶜ)ᶜ = (restrictPreimage s f '' t)ᶜ
[PROOFSTEP]
rw [← (congr_arg HasCompl.compl e).trans (compl_compl t)]
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : IsClosedMap f
t : Set ↑(f ⁻¹' s)
u : Set α
hu : IsOpen u
e : Subtype.val ⁻¹' u = tᶜ
⊢ Subtype.val ⁻¹' (f '' uᶜ)ᶜ = (restrictPreimage s f '' (Subtype.val ⁻¹' u)ᶜ)ᶜ
[PROOFSTEP]
simp only [Set.preimage_compl, compl_inj_iff]
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : IsClosedMap f
t : Set ↑(f ⁻¹' s)
u : Set α
hu : IsOpen u
e : Subtype.val ⁻¹' u = tᶜ
⊢ Subtype.val ⁻¹' (f '' uᶜ) = restrictPreimage s f '' (Subtype.val ⁻¹' u)ᶜ
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case mk.intro.intro.h.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : IsClosedMap f
t : Set ↑(f ⁻¹' s)
u : Set α
hu : IsOpen u
e : Subtype.val ⁻¹' u = tᶜ
x : β
hx : x ∈ s
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' (f '' uᶜ) ↔
    { val := x, property := hx } ∈ restrictPreimage s f '' (Subtype.val ⁻¹' u)ᶜ
[PROOFSTEP]
suffices (∃ y, y ∉ u ∧ f y = x) ↔ ∃ y, y ∉ u ∧ f y ∈ s ∧ f y = x by simpa [Set.restrictPreimage, ← Subtype.coe_inj]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : IsClosedMap f
t : Set ↑(f ⁻¹' s)
u : Set α
hu : IsOpen u
e : Subtype.val ⁻¹' u = tᶜ
x : β
hx : x ∈ s
this : (∃ y, ¬y ∈ u ∧ f y = x) ↔ ∃ y, ¬y ∈ u ∧ f y ∈ s ∧ f y = x
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' (f '' uᶜ) ↔
    { val := x, property := hx } ∈ restrictPreimage s f '' (Subtype.val ⁻¹' u)ᶜ
[PROOFSTEP]
simpa [Set.restrictPreimage, ← Subtype.coe_inj]
[GOAL]
case mk.intro.intro.h.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : IsClosedMap f
t : Set ↑(f ⁻¹' s)
u : Set α
hu : IsOpen u
e : Subtype.val ⁻¹' u = tᶜ
x : β
hx : x ∈ s
⊢ (∃ y, ¬y ∈ u ∧ f y = x) ↔ ∃ y, ¬y ∈ u ∧ f y ∈ s ∧ f y = x
[PROOFSTEP]
exact ⟨fun ⟨a, b, c⟩ => ⟨a, b, c.symm ▸ hx, c⟩, fun ⟨a, b, _, c⟩ => ⟨a, b, c⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
⊢ IsOpen s ↔ ∀ (i : ι), IsOpen (s ∩ ↑(U i))
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
⊢ IsOpen s → ∀ (i : ι), IsOpen (s ∩ ↑(U i))
[PROOFSTEP]
exact fun H i => H.inter (U i).2
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
⊢ (∀ (i : ι), IsOpen (s ∩ ↑(U i))) → IsOpen s
[PROOFSTEP]
intro H
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
⊢ IsOpen s
[PROOFSTEP]
have : ⋃ i, (U i : Set β) = Set.univ := by
  convert congr_arg (SetLike.coe) hU
  simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
⊢ ⋃ (i : ι), ↑(U i) = univ
[PROOFSTEP]
convert congr_arg (SetLike.coe) hU
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
⊢ ⋃ (i : ι), ↑(U i) = ↑(iSup U)
[PROOFSTEP]
simp
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
this : ⋃ (i : ι), ↑(U i) = univ
⊢ IsOpen s
[PROOFSTEP]
rw [← s.inter_univ, ← this, Set.inter_iUnion]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
this : ⋃ (i : ι), ↑(U i) = univ
⊢ IsOpen (⋃ (i : ι), s ∩ ↑(U i))
[PROOFSTEP]
exact isOpen_iUnion H
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
⊢ IsOpen s ↔ ∀ (i : ι), IsOpen (Subtype.val ⁻¹' s)
[PROOFSTEP]
rw [isOpen_iff_inter_of_iSup_eq_top hU s]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
⊢ (∀ (i : ι), IsOpen (s ∩ ↑(U i))) ↔ ∀ (i : ι), IsOpen (Subtype.val ⁻¹' s)
[PROOFSTEP]
refine forall_congr' fun i => ?_
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
i : ι
⊢ IsOpen (s ∩ ↑(U i)) ↔ IsOpen (Subtype.val ⁻¹' s)
[PROOFSTEP]
rw [(U _).2.openEmbedding_subtype_val.open_iff_image_open]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
i : ι
⊢ IsOpen (s ∩ ↑(U i)) ↔ IsOpen (Subtype.val '' (Subtype.val ⁻¹' s))
[PROOFSTEP]
erw [Set.image_preimage_eq_inter_range]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
i : ι
⊢ IsOpen (s ∩ ↑(U i)) ↔ IsOpen (s ∩ range Subtype.val)
[PROOFSTEP]
rw [Subtype.range_coe, Opens.carrier_eq_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
⊢ IsClosed s ↔ ∀ (i : ι), IsClosed (Subtype.val ⁻¹' s)
[PROOFSTEP]
simpa using isOpen_iff_coe_preimage_of_iSup_eq_top hU sᶜ
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
⊢ IsClosedMap f ↔ ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
[PROOFSTEP]
refine' ⟨fun h i => Set.restrictPreimage_isClosedMap _ h, _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
⊢ (∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)) → IsClosedMap f
[PROOFSTEP]
rintro H s hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
⊢ IsClosed (f '' s)
[PROOFSTEP]
rw [isClosed_iff_coe_preimage_of_iSup_eq_top hU]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
⊢ ∀ (i : ι), IsClosed (Subtype.val ⁻¹' (f '' s))
[PROOFSTEP]
intro i
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (restrictPreimage (U i).carrier f)
s : Set α
hs : IsClosed s
i : ι
⊢ IsClosed (Subtype.val ⁻¹' (f '' s))
[PROOFSTEP]
convert H i _ ⟨⟨_, hs.1, eq_compl_comm.mpr rfl⟩⟩
[GOAL]
case h.e'_3.h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
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ᶜ)ᶜ
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case h.e'_3.h.h.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
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ᶜ)ᶜ
[PROOFSTEP]
suffices (∃ y, y ∈ s ∧ f y = x) ↔ ∃ y, y ∈ s ∧ f y ∈ U i ∧ f y = x by simpa [Set.restrictPreimage, ← Subtype.coe_inj]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
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ᶜ)ᶜ
[PROOFSTEP]
simpa [Set.restrictPreimage, ← Subtype.coe_inj]
[GOAL]
case h.e'_3.h.h.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type u_3
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
[PROOFSTEP]
exact ⟨fun ⟨a, b, c⟩ => ⟨a, b, c.symm ▸ hx, c⟩, fun ⟨a, b, _, c⟩ => ⟨a, b, c⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Inducing f ↔ ∀ (i : ι), Inducing (restrictPreimage (U i).carrier f)
[PROOFSTEP]
simp_rw [inducing_subtype_val.inducing_iff, inducing_iff_nhds, restrictPreimage, MapsTo.coe_restrict, restrict_eq, ←
  @Filter.comap_comap _ _ _ _ _ f]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ (∀ (a : α), 𝓝 a = comap f (𝓝 (f a))) ↔
    ∀ (i : ι) (a : ↑(f ⁻¹' (U i).carrier)), 𝓝 a = comap Subtype.val (comap f (𝓝 ((f ∘ Subtype.val) a)))
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ (∀ (a : α), 𝓝 a = comap f (𝓝 (f a))) →
    ∀ (i : ι) (a : ↑(f ⁻¹' (U i).carrier)), 𝓝 a = comap Subtype.val (comap f (𝓝 ((f ∘ Subtype.val) a)))
[PROOFSTEP]
intro H i x
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
H : ∀ (a : α), 𝓝 a = comap f (𝓝 (f a))
i : ι
x : ↑(f ⁻¹' (U i).carrier)
⊢ 𝓝 x = comap Subtype.val (comap f (𝓝 ((f ∘ Subtype.val) x)))
[PROOFSTEP]
rw [Function.comp_apply, ← H, ← inducing_subtype_val.nhds_eq_comap]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ (∀ (i : ι) (a : ↑(f ⁻¹' (U i).carrier)), 𝓝 a = comap Subtype.val (comap f (𝓝 ((f ∘ Subtype.val) a)))) →
    ∀ (a : α), 𝓝 a = comap f (𝓝 (f a))
[PROOFSTEP]
intro H x
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
H : ∀ (i : ι) (a : ↑(f ⁻¹' (U i).carrier)), 𝓝 a = comap Subtype.val (comap f (𝓝 ((f ∘ Subtype.val) a)))
x : α
⊢ 𝓝 x = comap f (𝓝 (f x))
[PROOFSTEP]
obtain ⟨i, hi⟩ :=
  Opens.mem_iSup.mp
    (show f x ∈ iSup U by
      rw [hU]
      triv)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
H : ∀ (i : ι) (a : ↑(f ⁻¹' (U i).carrier)), 𝓝 a = comap Subtype.val (comap f (𝓝 ((f ∘ Subtype.val) a)))
x : α
⊢ f x ∈ iSup U
[PROOFSTEP]
rw [hU]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
H : ∀ (i : ι) (a : ↑(f ⁻¹' (U i).carrier)), 𝓝 a = comap Subtype.val (comap f (𝓝 ((f ∘ Subtype.val) a)))
x : α
⊢ f x ∈ ⊤
[PROOFSTEP]
triv
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
H : ∀ (i : ι) (a : ↑(f ⁻¹' (U i).carrier)), 𝓝 a = comap Subtype.val (comap f (𝓝 ((f ∘ Subtype.val) a)))
x : α
i : ι
hi : f x ∈ U i
⊢ 𝓝 x = comap f (𝓝 (f x))
[PROOFSTEP]
erw [← OpenEmbedding.map_nhds_eq (h.1 _ (U i).2).openEmbedding_subtype_val ⟨x, hi⟩]
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
H : ∀ (i : ι) (a : ↑(f ⁻¹' (U i).carrier)), 𝓝 a = comap Subtype.val (comap f (𝓝 ((f ∘ Subtype.val) a)))
x : α
i : ι
hi : f x ∈ U i
⊢ map Subtype.val (𝓝 { val := x, property := hi }) = comap f (𝓝 (f x))
[PROOFSTEP]
rw [(H i) ⟨x, hi⟩, Filter.subtype_coe_map_comap, Function.comp_apply, Subtype.coe_mk, inf_eq_left,
  Filter.le_principal_iff]
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
H : ∀ (i : ι) (a : ↑(f ⁻¹' (U i).carrier)), 𝓝 a = comap Subtype.val (comap f (𝓝 ((f ∘ Subtype.val) a)))
x : α
i : ι
hi : f x ∈ U i
⊢ f ⁻¹' (U i).carrier ∈ comap f (𝓝 (f x))
[PROOFSTEP]
exact Filter.preimage_mem_comap ((U i).2.mem_nhds hi)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Embedding f ↔ ∀ (i : ι), Embedding (restrictPreimage (U i).carrier f)
[PROOFSTEP]
simp_rw [embedding_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Inducing f ∧ Function.Injective f ↔
    ∀ (i : ι), Inducing (restrictPreimage (U i).carrier f) ∧ Function.Injective (restrictPreimage (U i).carrier f)
[PROOFSTEP]
rw [forall_and]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Inducing f ∧ Function.Injective f ↔
    (∀ (x : ι), Inducing (restrictPreimage (U x).carrier f)) ∧
      ∀ (x : ι), Function.Injective (restrictPreimage (U x).carrier f)
[PROOFSTEP]
apply and_congr
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Inducing f ↔ ∀ (x : ι), Inducing (restrictPreimage (U x).carrier f)
[PROOFSTEP]
apply inducing_iff_inducing_of_iSup_eq_top
[GOAL]
case h₁.hU
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ ⨆ (i : ι), U i = ⊤
[PROOFSTEP]
assumption
[GOAL]
case h₁.h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Continuous f
[PROOFSTEP]
assumption
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Function.Injective f ↔ ∀ (x : ι), Function.Injective (restrictPreimage (U x).carrier f)
[PROOFSTEP]
apply Set.injective_iff_injective_of_iUnion_eq_univ
[GOAL]
case h₂.hU
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ ⋃ (i : ι), (U i).carrier = univ
[PROOFSTEP]
convert congr_arg SetLike.coe hU
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ ⋃ (i : ι), (U i).carrier = ↑(iSup U)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ OpenEmbedding f ↔ ∀ (i : ι), OpenEmbedding (restrictPreimage (U i).carrier f)
[PROOFSTEP]
simp_rw [openEmbedding_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Embedding f ∧ IsOpen (range f) ↔
    ∀ (i : ι), Embedding (restrictPreimage (U i).carrier f) ∧ IsOpen (range (restrictPreimage (U i).carrier f))
[PROOFSTEP]
rw [forall_and]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Embedding f ∧ IsOpen (range f) ↔
    (∀ (x : ι), Embedding (restrictPreimage (U x).carrier f)) ∧
      ∀ (x : ι), IsOpen (range (restrictPreimage (U x).carrier f))
[PROOFSTEP]
apply and_congr
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Embedding f ↔ ∀ (x : ι), Embedding (restrictPreimage (U x).carrier f)
[PROOFSTEP]
apply embedding_iff_embedding_of_iSup_eq_top
[GOAL]
case h₁.hU
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ ⨆ (i : ι), U i = ⊤
[PROOFSTEP]
assumption
[GOAL]
case h₁.h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Continuous f
[PROOFSTEP]
assumption
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ IsOpen (range f) ↔ ∀ (x : ι), IsOpen (range (restrictPreimage (U x).carrier f))
[PROOFSTEP]
simp_rw [Set.range_restrictPreimage]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ IsOpen (range f) ↔ ∀ (x : ι), IsOpen (Subtype.val ⁻¹' range f)
[PROOFSTEP]
apply isOpen_iff_coe_preimage_of_iSup_eq_top hU
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ ClosedEmbedding f ↔ ∀ (i : ι), ClosedEmbedding (restrictPreimage (U i).carrier f)
[PROOFSTEP]
simp_rw [closedEmbedding_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Embedding f ∧ IsClosed (range f) ↔
    ∀ (i : ι), Embedding (restrictPreimage (U i).carrier f) ∧ IsClosed (range (restrictPreimage (U i).carrier f))
[PROOFSTEP]
rw [forall_and]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Embedding f ∧ IsClosed (range f) ↔
    (∀ (x : ι), Embedding (restrictPreimage (U x).carrier f)) ∧
      ∀ (x : ι), IsClosed (range (restrictPreimage (U x).carrier f))
[PROOFSTEP]
apply and_congr
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Embedding f ↔ ∀ (x : ι), Embedding (restrictPreimage (U x).carrier f)
[PROOFSTEP]
apply embedding_iff_embedding_of_iSup_eq_top
[GOAL]
case h₁.hU
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ ⨆ (i : ι), U i = ⊤
[PROOFSTEP]
assumption
[GOAL]
case h₁.h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Continuous f
[PROOFSTEP]
assumption
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ IsClosed (range f) ↔ ∀ (x : ι), IsClosed (range (restrictPreimage (U x).carrier f))
[PROOFSTEP]
simp_rw [Set.range_restrictPreimage]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type u_3
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ IsClosed (range f) ↔ ∀ (x : ι), IsClosed (Subtype.val ⁻¹' range f)
[PROOFSTEP]
apply isClosed_iff_coe_preimage_of_iSup_eq_top hU


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
hg : Inducing g
hf : Inducing f
⊢ inst✝³ = TopologicalSpace.induced (g ∘ f) inst✝¹
[PROOFSTEP]
rw [hf.induced, hg.induced, induced_compose]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hf : Continuous f
hg : Continuous g
hgf : Inducing (g ∘ f)
⊢ inst✝³ ≤ induced f inst✝²
[PROOFSTEP]
rwa [← continuous_iff_le_induced]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hf : Continuous f
hg : Continuous g
hgf : Inducing (g ∘ f)
⊢ induced f inst✝² ≤ inst✝³
[PROOFSTEP]
rw [hgf.induced, ← induced_compose]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hf : Continuous f
hg : Continuous g
hgf : Inducing (g ∘ f)
⊢ induced f inst✝² ≤ induced f (induced g inst✝¹)
[PROOFSTEP]
exact induced_mono hg.le_induced
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
⊢ 𝓝ˢ s = comap f (𝓝ˢ (f '' s))
[PROOFSTEP]
simp only [nhdsSet, sSup_image, comap_iSup, hf.nhds_eq_comap, iSup_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
a : α
l : Filter α
⊢ MapClusterPt (f a) l f ↔ ClusterPt a l
[PROOFSTEP]
delta MapClusterPt ClusterPt
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
a : α
l : Filter α
⊢ NeBot (𝓝 (f a) ⊓ map f l) ↔ NeBot (𝓝 a ⊓ l)
[PROOFSTEP]
rw [← Filter.push_pull', ← hf.nhds_eq_comap, map_neBot_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
ι : Type u_5
f : ι → β
g : β → γ
a : Filter ι
b : β
hg : Inducing g
⊢ Tendsto f a (𝓝 b) ↔ Tendsto (g ∘ f) a (𝓝 (g b))
[PROOFSTEP]
rw [hg.nhds_eq_comap, tendsto_comap_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
⊢ Continuous f ↔ Continuous (g ∘ f)
[PROOFSTEP]
simp_rw [continuous_iff_continuousAt, hg.continuousAt_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hf : Inducing f
x : α
h : range f ∈ 𝓝 (f x)
⊢ ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
[PROOFSTEP]
simp_rw [ContinuousAt, Filter.Tendsto, ← hf.map_nhds_of_mem _ h, Filter.map_map, comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
⊢ Inducing f ↔ Inducing (g ∘ f)
[PROOFSTEP]
refine' ⟨fun h => hg.comp h, fun hgf => inducing_of_inducing_compose _ hg.continuous hgf⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
hgf : Inducing (g ∘ f)
⊢ Continuous f
[PROOFSTEP]
rw [hg.continuous_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
hgf : Inducing (g ∘ f)
⊢ Continuous (g ∘ f)
[PROOFSTEP]
exact hgf.continuous
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
⊢ closure s = f ⁻¹' closure (f '' s)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
x : α
⊢ x ∈ closure s ↔ x ∈ f ⁻¹' closure (f '' s)
[PROOFSTEP]
rw [Set.mem_preimage, ← closure_induced, hf.induced]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
⊢ IsClosed s ↔ ∃ t, IsClosed t ∧ f ⁻¹' t = s
[PROOFSTEP]
rw [hf.induced, isClosed_induced_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
⊢ IsClosed s ↔ ∀ (x : α), f x ∈ closure (f '' s) → x ∈ s
[PROOFSTEP]
rw [hf.induced, isClosed_induced_iff']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
⊢ IsOpen s ↔ ∃ t, IsOpen t ∧ f ⁻¹' t = s
[PROOFSTEP]
rw [hf.induced, isOpen_induced_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
⊢ Dense s ↔ ∀ (x : α), f x ∈ closure (f '' s)
[PROOFSTEP]
simp only [Dense, hf.closure_eq_preimage_closure_image, mem_preimage]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hf : Continuous f
hg : Continuous g
hgf : _root_.Embedding (g ∘ f)
a₁ a₂ : α
h : f a₁ = f a₂
⊢ (g ∘ f) a₁ = (g ∘ f) a₂
[PROOFSTEP]
simp [h, (· ∘ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
X : Type u_5
Y : Type u_6
inst✝¹ : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DiscreteTopology Y
f : X → Y
hf : _root_.Embedding f
x : X
⊢ 𝓝 x = pure x
[PROOFSTEP]
rw [hf.nhds_eq_comap, nhds_discrete, comap_pure, ← image_singleton, hf.inj.preimage_image, principal_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
⊢ (∀ (x : Set β), IsOpen xᶜ ↔ IsOpen (f ⁻¹' xᶜ)) ↔ ∀ (s : Set β), IsClosed s ↔ IsClosed (f ⁻¹' s)
[PROOFSTEP]
simp only [isOpen_compl_iff, preimage_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
hg : QuotientMap g
hf : QuotientMap f
⊢ inst✝¹ = coinduced (g ∘ f) inst✝³
[PROOFSTEP]
rw [hg.right, hf.right, coinduced_compose]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
hf : Continuous f
hg : Continuous g
hgf : QuotientMap (g ∘ f)
⊢ inst✝¹ ≤ coinduced g inst✝²
[PROOFSTEP]
rw [hgf.right, ← coinduced_compose]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
hf : Continuous f
hg : Continuous g
hgf : QuotientMap (g ∘ f)
⊢ coinduced g (coinduced f inst✝³) ≤ coinduced g inst✝²
[PROOFSTEP]
exact coinduced_mono hf.coinduced_le
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
hf : QuotientMap f
⊢ Continuous g ↔ Continuous (g ∘ f)
[PROOFSTEP]
rw [continuous_iff_coinduced_le, continuous_iff_coinduced_le, hf.right, coinduced_compose]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
hs : IsOpen s
⊢ IsOpen (id '' s)
[PROOFSTEP]
rwa [image_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f✝ : α → β
g : β → γ
f : α → β
hg : IsOpenMap g
hf : IsOpenMap f
s : Set α
hs : IsOpen s
⊢ IsOpen (g ∘ f '' s)
[PROOFSTEP]
rw [image_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f✝ : α → β
g : β → γ
f : α → β
hg : IsOpenMap g
hf : IsOpenMap f
s : Set α
hs : IsOpen s
⊢ IsOpen (g '' (f '' s))
[PROOFSTEP]
exact hg _ (hf _ hs)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
⊢ IsOpen (range f)
[PROOFSTEP]
rw [← image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
⊢ IsOpen (f '' univ)
[PROOFSTEP]
exact hf _ isOpen_univ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f✝ f : α → β
h : ∀ (x : α), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ Function.RightInverse g f
x : α
g : β → α
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : Function.RightInverse g f
⊢ 𝓝 (f x) = map f (map g (𝓝 (f x)))
[PROOFSTEP]
rw [map_map, hgf.comp_eq_id, map_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f✝ f : α → β
h : ∀ (x : α), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ Function.RightInverse g f
x : α
g : β → α
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : Function.RightInverse g f
⊢ map f (𝓝 (g (f x))) = map f (𝓝 x)
[PROOFSTEP]
rw [hgx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
s : Set β
⊢ f ⁻¹' closure s ⊆ closure (f ⁻¹' s)
[PROOFSTEP]
rw [← compl_subset_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
s : Set β
⊢ (closure (f ⁻¹' s))ᶜ ⊆ (f ⁻¹' closure s)ᶜ
[PROOFSTEP]
simp only [← interior_compl, ← preimage_compl, hf.interior_preimage_subset_preimage_interior]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
s : Set β
⊢ f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s)
[PROOFSTEP]
simpa only [frontier_eq_closure_inter_closure, preimage_inter] using
  inter_subset_inter hf.preimage_closure_subset_closure_preimage hf.preimage_closure_subset_closure_preimage
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
hfc : Continuous f
s : Set β
⊢ f ⁻¹' frontier s = frontier (f ⁻¹' s)
[PROOFSTEP]
simp only [frontier_eq_closure_inter_closure, preimage_inter, preimage_compl,
  hf.preimage_closure_eq_closure_preimage hfc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hs : ∀ (s : Set α), f '' interior s ⊆ interior (f '' s)
u : Set α
hu : IsOpen u
⊢ f '' u = f '' interior u
[PROOFSTEP]
rw [hu.interior_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsClosed s
⊢ IsClosed (id '' s)
[PROOFSTEP]
rwa [image_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
hg : IsClosedMap g
hf : IsClosedMap f
⊢ IsClosedMap (g ∘ f)
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
hg : IsClosedMap g
hf : IsClosedMap f
s : Set α
hs : IsClosed s
⊢ IsClosed (g ∘ f '' s)
[PROOFSTEP]
rw [image_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
hg : IsClosedMap g
hf : IsClosedMap f
s : Set α
hs : IsClosed s
⊢ IsClosed (g '' (f '' s))
[PROOFSTEP]
exact hg _ (hf _ hs)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
f' : β → α
h : Continuous f'
l_inv : LeftInverse f f'
r_inv : Function.RightInverse f f'
s : Set α
hs : IsClosed s
⊢ IsClosed (f '' s)
[PROOFSTEP]
rw [image_eq_preimage_of_inverse r_inv l_inv]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
f' : β → α
h : Continuous f'
l_inv : LeftInverse f f'
r_inv : Function.RightInverse f f'
s : Set α
hs : IsClosed s
⊢ IsClosed (f' ⁻¹' s)
[PROOFSTEP]
exact hs.preimage h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h : ∀ (s : Set α), IsClosed s → Set.Nonempty s → IsClosed (f '' s)
⊢ IsClosedMap f
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h : ∀ (s : Set α), IsClosed s → Set.Nonempty s → IsClosed (f '' s)
s : Set α
hs : IsClosed s
⊢ IsClosed (f '' s)
[PROOFSTEP]
cases' eq_empty_or_nonempty s with h2s h2s
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h : ∀ (s : Set α), IsClosed s → Set.Nonempty s → IsClosed (f '' s)
s : Set α
hs : IsClosed s
h2s : s = ∅
⊢ IsClosed (f '' s)
[PROOFSTEP]
simp_rw [h2s, image_empty, isClosed_empty]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h : ∀ (s : Set α), IsClosed s → Set.Nonempty s → IsClosed (f '' s)
s : Set α
hs : IsClosed s
h2s : Set.Nonempty s
⊢ IsClosed (f '' s)
[PROOFSTEP]
exact h s hs h2s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Inducing f
h : IsClosed (range f)
⊢ IsClosedMap f
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Inducing f
h : IsClosed (range f)
s : Set α
hs : IsClosed s
⊢ IsClosed (f '' s)
[PROOFSTEP]
rcases hf.isClosed_iff.1 hs with ⟨t, ht, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Inducing f
h : IsClosed (range f)
t : Set β
ht : IsClosed t
hs : IsClosed (f ⁻¹' t)
⊢ IsClosed (f '' (f ⁻¹' t))
[PROOFSTEP]
rw [image_preimage_eq_inter_range]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Inducing f
h : IsClosed (range f)
t : Set β
ht : IsClosed t
hs : IsClosed (f ⁻¹' t)
⊢ IsClosed (t ∩ range f)
[PROOFSTEP]
exact ht.inter h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hs : ∀ (s : Set α), closure (f '' s) ⊆ f '' closure s
c : Set α
hc : IsClosed c
⊢ f '' closure c = f '' c
[PROOFSTEP]
rw [hc.closure_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
⊢ IsClosedMap f ↔ ∀ (s : Set α) (y : β), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
[PROOFSTEP]
simp [MapClusterPt, isClosedMap_iff_closure_image, subset_def, mem_closure_iff_clusterPt, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
f_closed : IsClosedMap f
f_cont : Continuous f
F : Filter α
⊢ Filter.lift' (map f F) closure = map f (Filter.lift' F closure)
[PROOFSTEP]
rw [map_lift'_eq2 (monotone_closure β), map_lift'_eq (monotone_closure α)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
f_closed : IsClosedMap f
f_cont : Continuous f
F : Filter α
⊢ Filter.lift' F (closure ∘ image f) = Filter.lift' F (image f ∘ closure)
[PROOFSTEP]
congr
[GOAL]
case e_h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
f_closed : IsClosedMap f
f_cont : Continuous f
F : Filter α
⊢ closure ∘ image f = image f ∘ closure
[PROOFSTEP]
ext s : 1
[GOAL]
case e_h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
f_closed : IsClosedMap f
f_cont : Continuous f
F : Filter α
s : Set α
⊢ (closure ∘ image f) s = (image f ∘ closure) s
[PROOFSTEP]
exact f_closed.closure_image_eq_of_continuous f_cont s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
F : Filter α
f : α → β
f_closed : IsClosedMap f
f_cont : Continuous f
y : β
⊢ MapClusterPt y F f ↔ NeBot (Filter.lift' F closure ⊓ 𝓟 (f ⁻¹' {y}))
[PROOFSTEP]
rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont, ← comap_principal, ←
  map_neBot_iff f, Filter.push_pull, principal_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : OpenEmbedding f
s : Set α
h : IsOpen (f '' s)
⊢ IsOpen s
[PROOFSTEP]
convert ← h.preimage hf.toEmbedding.continuous
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : OpenEmbedding f
s : Set α
h : IsOpen (f '' s)
⊢ f ⁻¹' (f '' s) = s
[PROOFSTEP]
apply preimage_image_eq _ hf.inj
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : OpenEmbedding f
g : β → γ
l : Filter γ
a : α
⊢ Tendsto (g ∘ f) (𝓝 a) l ↔ Tendsto g (𝓝 (f a)) l
[PROOFSTEP]
rw [Tendsto, ← map_map, hf.map_nhds_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : OpenEmbedding f
g : β → γ
l : Filter γ
a : α
⊢ map g (𝓝 (f a)) ≤ l ↔ Tendsto g (𝓝 (f a)) l
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : OpenEmbedding f
s : Set β
hs : s ⊆ range f
⊢ IsOpen s ↔ IsOpen (f ⁻¹' s)
[PROOFSTEP]
rw [hf.open_iff_image_open, image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ OpenEmbedding f
[PROOFSTEP]
simp only [openEmbedding_iff_embedding_open, embedding_iff, inducing_iff_nhds, *, and_true_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ ∀ (a : α), 𝓝 a = comap f (𝓝 (f a))
[PROOFSTEP]
exact fun a => le_antisymm (h₁.tendsto _).le_comap (@comap_map _ _ (𝓝 a) _ h₂ ▸ comap_mono (h₃.nhds_le _))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
hg : OpenEmbedding g
⊢ IsOpenMap f ↔ IsOpenMap (g ∘ f)
[PROOFSTEP]
simp_rw [isOpenMap_iff_nhds_le, ← map_map, comp, ← hg.map_nhds_eq, Filter.map_le_map_iff hg.inj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : OpenEmbedding g
⊢ OpenEmbedding (g ∘ f) ↔ OpenEmbedding f
[PROOFSTEP]
simp only [openEmbedding_iff_continuous_injective_open, ← hg.isOpenMap_iff, ← hg.1.continuous_iff, hg.inj.of_comp_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : ClosedEmbedding f
s : Set α
h : IsClosed (f '' s)
⊢ IsClosed s
[PROOFSTEP]
rw [← preimage_image_eq s hf.inj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : ClosedEmbedding f
s : Set α
h : IsClosed (f '' s)
⊢ IsClosed (f ⁻¹' (f '' s))
[PROOFSTEP]
exact h.preimage hf.continuous
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : ClosedEmbedding f
s : Set β
hs : s ⊆ range f
⊢ IsClosed s ↔ IsClosed (f ⁻¹' s)
[PROOFSTEP]
rw [hf.closed_iff_image_closed, image_preimage_eq_of_subset hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
⊢ ClosedEmbedding f
[PROOFSTEP]
refine closedEmbedding_of_embedding_closed ⟨⟨?_⟩, h₂⟩ h₃
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
⊢ inst✝² = induced f inst✝¹
[PROOFSTEP]
refine h₁.le_induced.antisymm fun s hs => ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set α
hs : IsOpen s
⊢ IsOpen s
[PROOFSTEP]
refine ⟨(f '' sᶜ)ᶜ, (h₃ _ hs.isClosed_compl).isOpen_compl, ?_⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set α
hs : IsOpen s
⊢ f ⁻¹' (f '' sᶜ)ᶜ = s
[PROOFSTEP]
rw [preimage_compl, preimage_image_eq _ h₂, compl_compl]