α : Type u
β : Type v
γ : Type ?u.37692
f : α → β
ι : Sort ?u.37699
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : t₁ ≤ induced f t₃
⊢ t₂ ≤ induced f t₃
α : Type u
β : Type v
γ : Type ?u.37692
f : α → β
ι : Sort ?u.37699
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : Continuous f
⊢ Continuous f
rw [continuous_iff_le_induced] at h₂ ⊢
no goals
α : Type u
β : Type v
γ : Type ?u.37692
f : α → β
ι : Sort ?u.37699
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : t₁ ≤ induced f t₃
⊢ t₂ ≤ induced f t₃
exact le_trans h₁ h₂