theorem
TopologicalSpace.prod_mono
{α : Type u_1}
{β : Type u_2}
{σ₁ σ₂ : TopologicalSpace α}
{τ₁ τ₂ : TopologicalSpace β}
(hσ : σ₁ ≤ σ₂)
(hτ : τ₁ ≤ τ₂)
:
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)
theorem
Continuous.piSemialgHomPi
{I : Type u_1}
{J : Type u_2}
{R : Type u_3}
{S : Type u_4}
(f : I → Type u_5)
(g : J → Type u_6)
[CommSemiring R]
[CommSemiring S]
{φ : R →+* S}
[(i : I) → Semiring (f i)]
[(i : I) → Algebra S (f i)]
[(j : J) → Semiring (g j)]
[(j : J) → Algebra R (g j)]
{r : I → J}
[(j : J) → TopologicalSpace (g j)]
[(i : I) → TopologicalSpace (f i)]
(p : (i : I) → g (r i) →ₛₐ[φ] f i)
(h : ∀ (i : I), Continuous ⇑(p i))
:
Continuous ⇑(Pi.semialgHomPi f g p)