α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : ∀ (x : β), ¬x ∈ s → f x = a
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 a) ↔ l ≤ comap f (𝓝 a)
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : ∀ (x : β), ¬x ∈ s → f x = a
⊢ Tendsto f (l ⊓ 𝓟 s) (𝓝 a) ↔ Tendsto f l (𝓝 a)
rw [tendsto_iff_comap, tendsto_iff_comap]
case h
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : ∀ (x : β), ¬x ∈ s → f x = a
⊢ 𝓟 (sᶜ) ≤ comap f (𝓝 a)

α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : 𝓟 (sᶜ) ≤ comap f (𝓝 a)
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 a) ↔ l ≤ comap f (𝓝 a)
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : ∀ (x : β), ¬x ∈ s → f x = a
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 a) ↔ l ≤ comap f (𝓝 a)
replace h : 𝓟 (sᶜ) ≤ comap f (𝓝 a)
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : 𝓟 (sᶜ) ≤ comap f (𝓝 a)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 a)
⊢ l ≤ comap f (𝓝 a)
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : 𝓟 (sᶜ) ≤ comap f (𝓝 a)
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 a) ↔ l ≤ comap f (𝓝 a)
refine' ⟨fun h' => _, le_trans inf_le_left⟩
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : 𝓟 (sᶜ) ≤ comap f (𝓝 a)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 a)
this : l ⊓ 𝓟 s ⊔ 𝓟 (sᶜ) ≤ comap f (𝓝 a)
⊢ l ≤ comap f (𝓝 a)
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : 𝓟 (sᶜ) ≤ comap f (𝓝 a)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 a)
⊢ l ≤ comap f (𝓝 a)
have := sup_le h' h
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : 𝓟 (sᶜ) ≤ comap f (𝓝 a)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 a)
this : l ≤ comap f (𝓝 a) ∧ 𝓟 (sᶜ) ≤ comap f (𝓝 a)
⊢ l ≤ comap f (𝓝 a)
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : 𝓟 (sᶜ) ≤ comap f (𝓝 a)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 a)
this : l ⊓ 𝓟 s ⊔ 𝓟 (sᶜ) ≤ comap f (𝓝 a)
⊢ l ≤ comap f (𝓝 a)
rw [sup_inf_right, sup_principal, union_compl_self, principal_univ, inf_top_eq, sup_le_iff]
  at this
no goals
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : 𝓟 (sᶜ) ≤ comap f (𝓝 a)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 a)
this : l ≤ comap f (𝓝 a) ∧ 𝓟 (sᶜ) ≤ comap f (𝓝 a)
⊢ l ≤ comap f (𝓝 a)
exact this.1
case h.intro.intro
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : ∀ (x : β), ¬x ∈ s → f x = a
U : Set β
t : Set α
ht : t ∈ 𝓝 a
htU : f ⁻¹' t ⊆ U
x : β
hx : x ∈ sᶜ
⊢ x ∈ U
case h
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : ∀ (x : β), ¬x ∈ s → f x = a
⊢ 𝓟 (sᶜ) ≤ comap f (𝓝 a)
rintro U ⟨t, ht, htU⟩ x hx
case h.intro.intro
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : ∀ (x : β), ¬x ∈ s → f x = a
U : Set β
t : Set α
ht : t ∈ 𝓝 a
htU : f ⁻¹' t ⊆ U
x : β
hx : x ∈ sᶜ
this : f x ∈ t
⊢ x ∈ U
case h.intro.intro
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : ∀ (x : β), ¬x ∈ s → f x = a
U : Set β
t : Set α
ht : t ∈ 𝓝 a
htU : f ⁻¹' t ⊆ U
x : β
hx : x ∈ sᶜ
⊢ x ∈ U
have : f x ∈ t := (h x hx).symm ▸ mem_of_mem_nhds ht
no goals
case h.intro.intro
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : ∀ (x : β), ¬x ∈ s → f x = a
U : Set β
t : Set α
ht : t ∈ 𝓝 a
htU : f ⁻¹' t ⊆ U
x : β
hx : x ∈ sᶜ
this : f x ∈ t
⊢ x ∈ U
exact htU this