α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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)))
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
U : ι → Opens β
hU : iSup U = ⊤
h : Continuous f
⊢ Inducing f ↔ ∀ (i : ι), Inducing (restrictPreimage (U i).carrier f)
simp_rw [inducing_subtype_val.inducing_iff, inducing_iff_nhds, restrictPreimage,
  MapsTo.coe_restrict, restrict_eq, ← @Filter.comap_comap _ _ _ _ _ f]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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)))

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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))
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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)))
constructor
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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)))
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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)))
intro H i x
no goals
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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)))
rw [Function.comp_apply, ← H, ← inducing_subtype_val.nhds_eq_comap]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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))
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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))
intro H x
case mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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))
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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))
obtain ⟨i, hi⟩ :=
  Opens.mem_iSup.mp
    (show f x ∈ iSup U by
      rw [hU]
      triv)
case mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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))
case mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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))
erw [← OpenEmbedding.map_nhds_eq (h.1 _ (U i).2).openEmbedding_subtype_val ⟨x, hi⟩]
case mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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))
case mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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))
rw [(H i) ⟨x, hi⟩, Filter.subtype_coe_map_comap, Function.comp_apply, Subtype.coe_mk,
  inf_eq_left, Filter.le_principal_iff]
no goals
case mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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))
exact Filter.preimage_mem_comap ((U i).2.mem_nhds hi)
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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 ∈ ⊤
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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
rw [hU]
no goals
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
ι : Type ?u.37607
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 ∈ ⊤
triv