α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
⊢ ∃ a, a ∈ f '' s ∧ ClusterPt a l
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
⊢ IsCompact (f '' s)
intro l lne ls
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
this : NeBot (comap f l ⊓ 𝓟 s)
⊢ ∃ a, a ∈ f '' s ∧ ClusterPt a l
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
⊢ ∃ a, a ∈ f '' s ∧ ClusterPt a l
have : NeBot (l.comap f ⊓ 𝓟 s) :=
  comap_inf_principal_neBot_of_image_mem lne (le_principal_iff.1 ls)
case intro.intro
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
this : NeBot (comap f l ⊓ 𝓟 s)
a : α
has : a ∈ s
ha : ClusterPt a (comap f l ⊓ 𝓟 s)
⊢ ∃ a, a ∈ f '' s ∧ ClusterPt a l
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
this : NeBot (comap f l ⊓ 𝓟 s)
⊢ ∃ a, a ∈ f '' s ∧ ClusterPt a l
obtain ⟨a, has, ha⟩ : ∃ a ∈ s, ClusterPt a (l.comap f ⊓ 𝓟 s) := @hs _ this inf_le_right
case intro.intro
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
this✝ : NeBot (comap f l ⊓ 𝓟 s)
a : α
has : a ∈ s
ha : ClusterPt a (comap f l ⊓ 𝓟 s)
this : NeBot (𝓝 a ⊓ (comap f l ⊓ 𝓟 s))
⊢ ∃ a, a ∈ f '' s ∧ ClusterPt a l
case intro.intro
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
this : NeBot (comap f l ⊓ 𝓟 s)
a : α
has : a ∈ s
ha : ClusterPt a (comap f l ⊓ 𝓟 s)
⊢ ∃ a, a ∈ f '' s ∧ ClusterPt a l
haveI := ha.neBot
case intro.intro
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
this✝ : NeBot (comap f l ⊓ 𝓟 s)
a : α
has : a ∈ s
ha : ClusterPt a (comap f l ⊓ 𝓟 s)
this : NeBot (𝓝 a ⊓ (comap f l ⊓ 𝓟 s))
⊢ ClusterPt (f a) l
case intro.intro
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
this✝ : NeBot (comap f l ⊓ 𝓟 s)
a : α
has : a ∈ s
ha : ClusterPt a (comap f l ⊓ 𝓟 s)
this : NeBot (𝓝 a ⊓ (comap f l ⊓ 𝓟 s))
⊢ ∃ a, a ∈ f '' s ∧ ClusterPt a l
use f a, mem_image_of_mem f has
case intro.intro
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
this✝¹ : NeBot (comap f l ⊓ 𝓟 s)
a : α
has : a ∈ s
ha : ClusterPt a (comap f l ⊓ 𝓟 s)
this✝ : NeBot (𝓝 a ⊓ (comap f l ⊓ 𝓟 s))
this : Tendsto f (𝓝 a ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f a) ⊓ l)
⊢ ClusterPt (f a) l
case intro.intro
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
this✝ : NeBot (comap f l ⊓ 𝓟 s)
a : α
has : a ∈ s
ha : ClusterPt a (comap f l ⊓ 𝓟 s)
this : NeBot (𝓝 a ⊓ (comap f l ⊓ 𝓟 s))
⊢ ClusterPt (f a) l
have : Tendsto f (𝓝 a ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f a) ⊓ l) := by
  convert (hf a has).inf (@tendsto_comap _ _ f l) using 1
  rw [nhdsWithin]
  ac_rfl
no goals
case intro.intro
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
this✝¹ : NeBot (comap f l ⊓ 𝓟 s)
a : α
has : a ∈ s
ha : ClusterPt a (comap f l ⊓ 𝓟 s)
this✝ : NeBot (𝓝 a ⊓ (comap f l ⊓ 𝓟 s))
this : Tendsto f (𝓝 a ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f a) ⊓ l)
⊢ ClusterPt (f a) l
exact this.neBot
case h.e'_4
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
this✝ : NeBot (comap f l ⊓ 𝓟 s)
a : α
has : a ∈ s
ha : ClusterPt a (comap f l ⊓ 𝓟 s)
this : NeBot (𝓝 a ⊓ (comap f l ⊓ 𝓟 s))
⊢ 𝓝 a ⊓ (comap f l ⊓ 𝓟 s) = 𝓝[s] a ⊓ comap f l
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
this✝ : NeBot (comap f l ⊓ 𝓟 s)
a : α
has : a ∈ s
ha : ClusterPt a (comap f l ⊓ 𝓟 s)
this : NeBot (𝓝 a ⊓ (comap f l ⊓ 𝓟 s))
⊢ Tendsto f (𝓝 a ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f a) ⊓ l)
convert (hf a has).inf (@tendsto_comap _ _ f l) using 1
case h.e'_4
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
this✝ : NeBot (comap f l ⊓ 𝓟 s)
a : α
has : a ∈ s
ha : ClusterPt a (comap f l ⊓ 𝓟 s)
this : NeBot (𝓝 a ⊓ (comap f l ⊓ 𝓟 s))
⊢ 𝓝 a ⊓ (comap f l ⊓ 𝓟 s) = 𝓝 a ⊓ 𝓟 s ⊓ comap f l
case h.e'_4
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
this✝ : NeBot (comap f l ⊓ 𝓟 s)
a : α
has : a ∈ s
ha : ClusterPt a (comap f l ⊓ 𝓟 s)
this : NeBot (𝓝 a ⊓ (comap f l ⊓ 𝓟 s))
⊢ 𝓝 a ⊓ (comap f l ⊓ 𝓟 s) = 𝓝[s] a ⊓ comap f l
rw [nhdsWithin]
no goals
case h.e'_4
α : Type u
β : Type v
ι : Type ?u.7857
π : ι → Type ?u.7862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
l : Filter β
lne : NeBot l
ls : l ≤ 𝓟 (f '' s)
this✝ : NeBot (comap f l ⊓ 𝓟 s)
a : α
has : a ∈ s
ha : ClusterPt a (comap f l ⊓ 𝓟 s)
this : NeBot (𝓝 a ⊓ (comap f l ⊓ 𝓟 s))
⊢ 𝓝 a ⊓ (comap f l ⊓ 𝓟 s) = 𝓝 a ⊓ 𝓟 s ⊓ comap f l
ac_rfl