α : Type u
β : Type v
γ : Type w
δ : Type ?u.313560
ι : Sort x
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ g ≤ map φ (map ψ g)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.313560
ι : Sort x
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ map φ f = g
refine' le_antisymm hφ (le_trans _ (map_mono hψ))
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.313560
ι : Sort x
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ g ≤ map φ (map ψ g)
rw [map_map, eq, map_id]