α : Type u
β : Type v
γ : Type ?u.37963
f : α → β
ι : Sort ?u.37970
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₃
h₂ : coinduced f t₁ ≤ t₂
⊢ coinduced f t₁ ≤ t₃
α : Type u
β : Type v
γ : Type ?u.37963
f : α → β
ι : Sort ?u.37970
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₃
h₂ : Continuous f
⊢ Continuous f
rw [continuous_iff_coinduced_le] at h₂ ⊢
no goals
α : Type u
β : Type v
γ : Type ?u.37963
f : α → β
ι : Sort ?u.37970
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₃
h₂ : coinduced f t₁ ≤ t₂
⊢ coinduced f t₁ ≤ t₃
exact le_trans h₂ h₁