ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
H : ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l
s : Set β
hs : s ∈ l
⊢ s ∈ map f k
ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
⊢ Tendsto f k l ↔ ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l
refine' ⟨fun h x hx => h.comp hx, fun H s hs => _⟩
ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
H : ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l
s : Set β
hs : s ∈ l
⊢ s ∈ map f k
contrapose! H
ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
this : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
have : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ)) := by simpa [neBot_iff, inf_principal_eq_bot]
case intro
ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
this : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
x : ℕ → α
hx : Tendsto x atTop (k ⊓ 𝓟 (f ⁻¹' sᶜ))
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
this : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
rcases (k ⊓ 𝓟 (f ⁻¹' sᶜ)).exists_seq_tendsto with ⟨x, hx⟩
case intro
ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
this : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
case intro
ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
this : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
x : ℕ → α
hx : Tendsto x atTop (k ⊓ 𝓟 (f ⁻¹' sᶜ))
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
rw [tendsto_inf, tendsto_principal] at hx
case intro
ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
this : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
h : Tendsto (f ∘ x) atTop l
⊢ False
case intro
ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
this : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
refine' ⟨x, hx.1, fun h => _⟩
case intro.intro.intro
ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
this : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
h : Tendsto (f ∘ x) atTop l
N : ℕ
hnmem : x N ∈ f ⁻¹' sᶜ
hmem : (f ∘ x) N ∈ s
⊢ False
case intro
ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
this : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
h : Tendsto (f ∘ x) atTop l
⊢ False
rcases (hx.2.and (h hs)).exists with ⟨N, hnmem, hmem⟩
no goals
case intro.intro.intro
ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
this : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
h : Tendsto (f ∘ x) atTop l
N : ℕ
hnmem : x N ∈ f ⁻¹' sᶜ
hmem : (f ∘ x) N ∈ s
⊢ False
exact hnmem hmem
no goals
ι : Type ?u.364855
ι' : Type ?u.364858
α : Type u_1
β : Type u_2
γ : Type ?u.364867
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
⊢ NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
simpa [neBot_iff, inf_principal_eq_bot]