α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
δ : Type u_2
F : Filter ι
φ : δ → ι
p : Filter δ
x : α
u : ι → α
inst✝ : NeBot p
h : Tendsto φ p F
H : Tendsto (u ∘ φ) p (𝓝 x)
this : map (u ∘ φ) p ≤ map u F
⊢ MapClusterPt x F u
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
δ : Type u_2
F : Filter ι
φ : δ → ι
p : Filter δ
x : α
u : ι → α
inst✝ : NeBot p
h : Tendsto φ p F
H : Tendsto (u ∘ φ) p (𝓝 x)
⊢ MapClusterPt x F u
have :=
  calc
    map (u ∘ φ) p = map u (map φ p) := map_map
    _ ≤ map u F := map_mono h
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
δ : Type u_2
F : Filter ι
φ : δ → ι
p : Filter δ
x : α
u : ι → α
inst✝ : NeBot p
h : Tendsto φ p F
H : Tendsto (u ∘ φ) p (𝓝 x)
this✝ : map (u ∘ φ) p ≤ map u F
this : map (u ∘ φ) p ≤ 𝓝 x ⊓ map u F
⊢ MapClusterPt x F u
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
δ : Type u_2
F : Filter ι
φ : δ → ι
p : Filter δ
x : α
u : ι → α
inst✝ : NeBot p
h : Tendsto φ p F
H : Tendsto (u ∘ φ) p (𝓝 x)
this : map (u ∘ φ) p ≤ map u F
⊢ MapClusterPt x F u
have : map (u ∘ φ) p ≤ 𝓝 x ⊓ map u F := le_inf H this
no goals
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
δ : Type u_2
F : Filter ι
φ : δ → ι
p : Filter δ
x : α
u : ι → α
inst✝ : NeBot p
h : Tendsto φ p F
H : Tendsto (u ∘ φ) p (𝓝 x)
this✝ : map (u ∘ φ) p ≤ map u F
this : map (u ∘ φ) p ≤ 𝓝 x ⊓ map u F
⊢ MapClusterPt x F u
exact neBot_of_le this