α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
⊢ ∀ (t : Set β), t ∈ 𝓝 (f x) ↔ ∃ i, p i ∧ closure (f '' s i) ⊆ t
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : HasBasis (𝓝 x) p s
f : α → β
hf : DenseInducing f
⊢ HasBasis (𝓝 (f x)) p fun i => closure (f '' s i)
rw [Filter.hasBasis_iff] at h⊢
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
⊢ T ∈ 𝓝 (f x) ↔ ∃ i, p i ∧ closure (f '' s i) ⊆ T
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
⊢ ∀ (t : Set β), t ∈ 𝓝 (f x) ↔ ∃ i, p i ∧ closure (f '' s i) ⊆ t
intro T
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T

case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : ∃ i, p i ∧ closure (f '' s i) ⊆ T
⊢ T ∈ 𝓝 (f x)
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
⊢ T ∈ 𝓝 (f x) ↔ ∃ i, p i ∧ closure (f '' s i) ⊆ T
refine' ⟨fun hT => _, fun hT => _⟩
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T
obtain ⟨T', hT₁, hT₂, hT₃⟩ := exists_mem_nhds_isClosed_subset hT
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
hT₄ : f ⁻¹' T' ∈ 𝓝 x
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T
have hT₄ : f ⁻¹' T' ∈ 𝓝 x := by
  rw [hf.toInducing.nhds_eq_comap x]
  exact ⟨T', hT₁, Subset.rfl⟩
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
hT₄ : f ⁻¹' T' ∈ 𝓝 x
i : ι
hi : p i
hi' : s i ⊆ f ⁻¹' T'
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
hT₄ : f ⁻¹' T' ∈ 𝓝 x
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T
obtain ⟨i, hi, hi'⟩ := (h _).mp hT₄
no goals
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
hT₄ : f ⁻¹' T' ∈ 𝓝 x
i : ι
hi : p i
hi' : s i ⊆ f ⁻¹' T'
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T
exact
  ⟨i, hi,
    (closure_mono (image_subset f hi')).trans
      (Subset.trans (closure_minimal (image_preimage_subset _ _) hT₂) hT₃)⟩
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
⊢ f ⁻¹' T' ∈ Filter.comap f (𝓝 (f x))
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
⊢ f ⁻¹' T' ∈ 𝓝 x
rw [hf.toInducing.nhds_eq_comap x]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
⊢ f ⁻¹' T' ∈ Filter.comap f (𝓝 (f x))
exact ⟨T', hT₁, Subset.rfl⟩
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
⊢ T ∈ 𝓝 (f x)
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : ∃ i, p i ∧ closure (f '' s i) ⊆ T
⊢ T ∈ 𝓝 (f x)
obtain ⟨i, hi, hi'⟩ := hT
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
⊢ closure (f '' s i) ∈ 𝓝 (f x)
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
⊢ T ∈ 𝓝 (f x)
suffices closure (f '' s i) ∈ 𝓝 (f x) by filter_upwards [this]using hi'
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
f : α → β
hf : DenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
h : s i ∈ 𝓝 x
⊢ closure (f '' s i) ∈ 𝓝 (f x)
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
⊢ closure (f '' s i) ∈ 𝓝 (f x)
replace h := (h (s i)).mpr ⟨i, hi, Subset.rfl⟩
no goals
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
f : α → β
hf : DenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
h : s i ∈ 𝓝 x
⊢ closure (f '' s i) ∈ 𝓝 (f x)
exact hf.closure_image_mem_nhds h
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.42701
δ : Type ?u.42704
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_3
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
this : closure (f '' s i) ∈ 𝓝 (f x)
⊢ T ∈ 𝓝 (f x)
filter_upwards [this]using hi'