theorem TopologicalSpace.prod_mono {α : Type u_1} {β : Type u_2} {σ₁ σ₂ : TopologicalSpace α} {τ₁ τ₂ : TopologicalSpace β} (hσ : σ₁ ≤ σ₂) (hτ : τ₁ ≤ τ₂) : instTopologicalSpaceProd ≤ instTopologicalSpaceProd

theorem DenseRange.codRestrict_comp {Y : Type u_1} {Z : Type u_2} [TopologicalSpace Y] [TopologicalSpace Z] {α : Type u_3} {g : Y → Z} {f : α → Y} (hf : DenseRange f) (cg : Continuous g) : DenseRange (Set.codRestrict g (Set.range g) ⋯ ∘ f)