α : Type u
β : Type v
γ : Type w
δ : Type ?u.313181
ι : Sort x
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap φ (comap ψ f) ≤ f
α : Type u
β : Type v
γ : Type w
δ : Type ?u.313181
ι : Sort x
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap φ g = f
refine' ((comap_mono <| map_le_iff_le_comap.1 hψ).trans _).antisymm (map_le_iff_le_comap.1 hφ)
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.313181
ι : Sort x
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap φ (comap ψ f) ≤ f
rw [comap_comap, eq, comap_id]