[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
