Constructions #
Material destined for Mathlib.
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)
theorem
continuous_of_discreteTopology_snd
{X : Type u_1}
{D : Type u_2}
{Y : Type u_3}
[TopologicalSpace X]
[TopologicalSpace D]
[DiscreteTopology D]
[TopologicalSpace Y]
{g : X × D → Y}
(hg : ∀ (d : D), Continuous fun (x : X) => g (x, d))
:
A map on X × D with D discrete is continuous as soon as all its slices x ↦ g (x, d)
are continuous.