Constructions of new topological spaces from old ones #
This file constructs pi types, subtypes and quotients of topological spaces and sets up their basic theory, such as criteria for maps into or out of these constructions to be continuous; descriptions of the open sets, neighborhood filters, and generators of these constructions; and their behavior with respect to embeddings and other specific classes of maps.
Implementation note #
The constructed topologies are defined using induced and coinduced topologies
along with the complete lattice structure on topologies. Their universal properties
(for example, a map X → Y × Z is continuous if and only if both projections
X → Y, X → Z are) follow easily using order-theoretic descriptions of
continuity. With more work we can also extract descriptions of the open sets,
neighborhood filters and so on.
Tags #
product, subspace, quotient space
instance
instTopologicalSpaceQuot
{X : Type u}
{r : X → X → Prop}
[t : TopologicalSpace X]
:
TopologicalSpace (Quot r)
Equations
instance
instTopologicalSpaceSigma
{ι : Type u_5}
{X : ι → Type v}
[t₂ : (i : ι) → TopologicalSpace (X i)]
:
Equations
- instTopologicalSpaceSigma = ⨆ (i : ι), TopologicalSpace.coinduced (Sigma.mk i) (t₂ i)
instance
Pi.topologicalSpace
{ι : Type u_5}
{Y : ι → Type v}
[t₂ : (i : ι) → TopologicalSpace (Y i)]
:
TopologicalSpace ((i : ι) → Y i)
Equations
- Pi.topologicalSpace = ⨅ (i : ι), TopologicalSpace.induced (fun (f : (i : ι) → Y i) => f i) (t₂ i)
Additive, Multiplicative #
The topology on those type synonyms is inherited without change.
Equations
Equations
instance
instDiscreteTopologyMultiplicative
{X : Type u}
[TopologicalSpace X]
[DiscreteTopology X]
:
Order dual #
The topology on this type synonym is inherited without change.
Equations
instance
OrderDual.instNeBotNhdsWithinIoi
{X : Type u}
[TopologicalSpace X]
[Preorder X]
{x : X}
[(nhdsWithin x (Set.Iio x)).NeBot]
:
(nhdsWithin (toDual x) (Set.Ioi (toDual x))).NeBot
instance
OrderDual.instNeBotNhdsWithinIio
{X : Type u}
[TopologicalSpace X]
[Preorder X]
{x : X}
[(nhdsWithin x (Set.Ioi x)).NeBot]
:
(nhdsWithin (toDual x) (Set.Iio (toDual x))).NeBot
theorem
Quotient.preimage_mem_nhds
{X : Type u}
[TopologicalSpace X]
[s : Setoid X]
{V : Set (Quotient s)}
{x : X}
(hs : V ∈ nhds (Quotient.mk' x))
:
theorem
Dense.quotient
{X : Type u}
[Setoid X]
[TopologicalSpace X]
{s : Set X}
(H : Dense s)
:
Dense (Quotient.mk' '' s)
The image of a dense set under Quotient.mk' is a dense set.
theorem
DenseRange.quotient
{X : Type u}
{Y : Type v}
[Setoid X]
[TopologicalSpace X]
{f : Y → X}
(hf : DenseRange f)
:
DenseRange (Quotient.mk' ∘ f)
The composition of Quotient.mk' and a function with dense range has dense range.
theorem
continuous_map_sInf
{α : Type u_5}
[TopologicalSpace α]
{S : Set (Setoid α)}
{s : Setoid α}
(h : s ∈ S)
:
instance
instDiscreteTopologySubtype
{X : Type u}
{p : X → Prop}
[TopologicalSpace X]
[DiscreteTopology X]
:
instance
Sum.discreteTopology
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
[h : DiscreteTopology X]
[hY : DiscreteTopology Y]
:
DiscreteTopology (X ⊕ Y)
instance
Sigma.discreteTopology
{ι : Type u_5}
{Y : ι → Type v}
[(i : ι) → TopologicalSpace (Y i)]
[h : ∀ (i : ι), DiscreteTopology (Y i)]
:
@[simp]
theorem
comap_nhdsWithin_range
{α : Type u_5}
{β : Type u_6}
[TopologicalSpace β]
(f : α → β)
(y : β)
:
theorem
nhds_subtype_eq_comap_nhdsWithin
{X : Type u}
[TopologicalSpace X]
(s : Set X)
(x : { x : X // x ∈ s })
:
A type synonym equipped with the topology whose open sets are the empty set and the sets with finite complements.
Equations
- CofiniteTopology X = X
Instances For
Equations
- CofiniteTopology.instInhabited = { default := CofiniteTopology.of default }
Equations
- CofiniteTopology.instTopologicalSpace = { IsOpen := fun (s : Set (CofiniteTopology X)) => s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }
theorem
CofiniteTopology.mem_nhds_iff
{X : Type u}
{x : CofiniteTopology X}
{s : Set (CofiniteTopology X)}
:
instance
Prod.instNeBotNhdsWithinIoi
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
[Preorder X]
[Preorder Y]
{x : X × Y}
[(nhdsWithin x.1 (Set.Ioi x.1)).NeBot]
[(nhdsWithin x.2 (Set.Ioi x.2)).NeBot]
:
(nhdsWithin x (Set.Ioi x)).NeBot
theorem
MapClusterPt.curry_prodMap
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{α : Type u_5}
{β : Type u_6}
{f : α → X}
{g : β → Y}
{la : Filter α}
{lb : Filter β}
{x : X}
{y : Y}
(hf : MapClusterPt x la f)
(hg : MapClusterPt y lb g)
:
theorem
MapClusterPt.prodMap
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{α : Type u_5}
{β : Type u_6}
{f : α → X}
{g : β → Y}
{la : Filter α}
{lb : Filter β}
{x : X}
{y : Y}
(hf : MapClusterPt x la f)
(hg : MapClusterPt y lb g)
:
@[deprecated Topology.IsInducing.subtypeVal (since := "2024-10-28")]
Alias of Topology.IsInducing.subtypeVal.
theorem
Topology.IsInducing.of_codRestrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{t : Set Y}
(ht : ∀ (x : X), f x ∈ t)
(h : IsInducing (Set.codRestrict f t ht))
:
@[deprecated Topology.IsInducing.of_codRestrict (since := "2024-10-28")]
theorem
Inducing.of_codRestrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{t : Set Y}
(ht : ∀ (x : X), f x ∈ t)
(h : Topology.IsInducing (Set.codRestrict f t ht))
:
Alias of Topology.IsInducing.of_codRestrict.
@[deprecated Topology.IsEmbedding.subtypeVal (since := "2024-10-26")]
Alias of Topology.IsEmbedding.subtypeVal.
theorem
Topology.IsClosedEmbedding.subtypeVal
{X : Type u}
[TopologicalSpace X]
{p : X → Prop}
(h : IsClosed {a : X | p a})
:
@[deprecated Topology.IsClosedEmbedding.subtypeVal (since := "2024-10-20")]
theorem
closedEmbedding_subtype_val
{X : Type u}
[TopologicalSpace X]
{p : X → Prop}
(h : IsClosed {a : X | p a})
:
Alias of Topology.IsClosedEmbedding.subtypeVal.
theorem
Continuous.subtype_val
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{p : X → Prop}
{f : Y → Subtype p}
(hf : Continuous f)
:
Continuous fun (x : Y) => ↑(f x)
theorem
IsOpen.isOpenEmbedding_subtypeVal
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(hs : IsOpen s)
:
@[deprecated IsOpen.isOpenEmbedding_subtypeVal (since := "2024-10-18")]
theorem
IsOpen.openEmbedding_subtype_val
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(hs : IsOpen s)
:
Alias of IsOpen.isOpenEmbedding_subtypeVal.
theorem
IsOpen.isOpenMap_subtype_val
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(hs : IsOpen s)
:
theorem
IsOpenMap.restrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : IsOpenMap f)
{s : Set X}
(hs : IsOpen s)
:
theorem
IsClosed.isClosedEmbedding_subtypeVal
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(hs : IsClosed s)
:
@[deprecated IsClosed.isClosedEmbedding_subtypeVal (since := "2024-10-20")]
theorem
IsClosed.closedEmbedding_subtype_val
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(hs : IsClosed s)
:
Alias of IsClosed.isClosedEmbedding_subtypeVal.
theorem
IsClosed.isClosedMap_subtype_val
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(hs : IsClosed s)
:
theorem
Continuous.subtype_mk
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{p : X → Prop}
{f : Y → X}
(h : Continuous f)
(hp : ∀ (x : Y), p (f x))
:
Continuous fun (x : Y) => ⟨f x, ⋯⟩
theorem
Continuous.subtype_map
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{p : X → Prop}
{f : X → Y}
(h : Continuous f)
{q : Y → Prop}
(hpq : ∀ (x : X), p x → q (f x))
:
Continuous (Subtype.map f hpq)
theorem
map_nhds_subtype_coe_eq_nhds
{X : Type u}
[TopologicalSpace X]
{p : X → Prop}
{x : X}
(hx : p x)
(h : ∀ᶠ (x : X) in nhds x, p x)
:
theorem
tendsto_subtype_rng
{X : Type u}
[TopologicalSpace X]
{Y : Type u_5}
{p : X → Prop}
{l : Filter Y}
{f : Y → Subtype p}
{x : Subtype p}
:
@[simp]
theorem
continuousAt_codRestrict_iff
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{t : Set Y}
(h1 : ∀ (x : X), f x ∈ t)
{x : X}
:
theorem
ContinuousAt.codRestrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{t : Set Y}
(h1 : ∀ (x : X), f x ∈ t)
{x : X}
:
ContinuousAt f x → ContinuousAt (Set.codRestrict f t h1) x
Alias of the reverse direction of continuousAt_codRestrict_iff.
theorem
ContinuousAt.restrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set X}
{t : Set Y}
(h1 : Set.MapsTo f s t)
{x : ↑s}
(h2 : ContinuousAt f ↑x)
:
ContinuousAt (Set.MapsTo.restrict f s t h1) x
theorem
ContinuousAt.restrictPreimage
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set Y}
{x : ↑(f ⁻¹' s)}
(h : ContinuousAt f ↑x)
:
ContinuousAt (s.restrictPreimage f) x
theorem
Continuous.codRestrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set Y}
(hf : Continuous f)
(hs : ∀ (a : X), f a ∈ s)
:
Continuous (Set.codRestrict f s hs)
theorem
Continuous.restrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set X}
{t : Set Y}
(h1 : Set.MapsTo f s t)
(h2 : Continuous f)
:
Continuous (Set.MapsTo.restrict f s t h1)
theorem
Continuous.restrictPreimage
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set Y}
(h : Continuous f)
:
Continuous (s.restrictPreimage f)
theorem
Topology.IsInducing.codRestrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{e : X → Y}
(he : IsInducing e)
{s : Set Y}
(hs : ∀ (x : X), e x ∈ s)
:
IsInducing (Set.codRestrict e s hs)
@[deprecated Topology.IsInducing.codRestrict (since := "2024-10-28")]
theorem
Inducing.codRestrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{e : X → Y}
(he : Topology.IsInducing e)
{s : Set Y}
(hs : ∀ (x : X), e x ∈ s)
:
Topology.IsInducing (Set.codRestrict e s hs)
Alias of Topology.IsInducing.codRestrict.
theorem
Topology.IsEmbedding.codRestrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{e : X → Y}
(he : IsEmbedding e)
(s : Set Y)
(hs : ∀ (x : X), e x ∈ s)
:
IsEmbedding (Set.codRestrict e s hs)
@[deprecated Topology.IsEmbedding.codRestrict (since := "2024-10-26")]
theorem
Embedding.codRestrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{e : X → Y}
(he : Topology.IsEmbedding e)
(s : Set Y)
(hs : ∀ (x : X), e x ∈ s)
:
Topology.IsEmbedding (Set.codRestrict e s hs)
Alias of Topology.IsEmbedding.codRestrict.
theorem
Topology.IsEmbedding.inclusion
{X : Type u}
[TopologicalSpace X]
{s t : Set X}
(h : s ⊆ t)
:
theorem
Topology.IsOpenEmbedding.inclusion
{X : Type u}
[TopologicalSpace X]
{s t : Set X}
(hst : s ⊆ t)
(hs : IsOpen (Subtype.val ⁻¹' s))
:
IsOpenEmbedding (Set.inclusion hst)
theorem
Topology.IsClosedEmbedding.inclusion
{X : Type u}
[TopologicalSpace X]
{s t : Set X}
(hst : s ⊆ t)
(hs : IsClosed (Subtype.val ⁻¹' s))
:
@[deprecated Topology.IsEmbedding.inclusion (since := "2024-10-26")]
Alias of Topology.IsEmbedding.inclusion.
theorem
DiscreteTopology.of_subset
{X : Type u_5}
[TopologicalSpace X]
{s t : Set X}
:
DiscreteTopology ↑s → ∀ (ts : t ⊆ s), DiscreteTopology ↑t
Let s, t ⊆ X be two subsets of a topological space X. If t ⊆ s and the topology induced
by Xon s is discrete, then also the topology induces on t is discrete.
theorem
DiscreteTopology.preimage_of_continuous_injective
{X : Type u_5}
{Y : Type u_6}
[TopologicalSpace X]
[TopologicalSpace Y]
(s : Set Y)
[DiscreteTopology ↑s]
{f : X → Y}
(hc : Continuous f)
(hinj : Function.Injective f)
:
DiscreteTopology ↑(f ⁻¹' s)
Let s be a discrete subset of a topological space. Then the preimage of s by
a continuous injective map is also discrete.
theorem
Topology.IsQuotientMap.restrictPreimage_isOpen
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : IsQuotientMap f)
{s : Set Y}
(hs : IsOpen s)
:
If f : X → Y is a quotient map,
then its restriction to the preimage of an open set is a quotient map too.
@[deprecated Topology.IsQuotientMap.restrictPreimage_isOpen (since := "2024-10-22")]
theorem
QuotientMap.restrictPreimage_isOpen
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : Topology.IsQuotientMap f)
{s : Set Y}
(hs : IsOpen s)
:
Alias of Topology.IsQuotientMap.restrictPreimage_isOpen.
If f : X → Y is a quotient map,
then its restriction to the preimage of an open set is a quotient map too.
theorem
IsOpen.preimage_val
{X : Type u}
[TopologicalSpace X]
{s t : Set X}
(ht : IsOpen t)
:
IsOpen (Subtype.val ⁻¹' t)
theorem
IsClosed.preimage_val
{X : Type u}
[TopologicalSpace X]
{s t : Set X}
(ht : IsClosed t)
:
IsClosed (Subtype.val ⁻¹' t)
@[simp]
theorem
IsOpen.inter_preimage_val_iff
{X : Type u}
[TopologicalSpace X]
{s t : Set X}
(hs : IsOpen s)
:
@[simp]
theorem
IsClosed.inter_preimage_val_iff
{X : Type u}
[TopologicalSpace X]
{s t : Set X}
(hs : IsClosed s)
:
@[deprecated isQuotientMap_quot_mk (since := "2024-10-22")]
Alias of isQuotientMap_quot_mk.
theorem
continuous_quot_mk
{X : Type u}
[TopologicalSpace X]
{r : X → X → Prop}
:
Continuous (Quot.mk r)
theorem
continuous_quot_lift
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{r : X → X → Prop}
{f : X → Y}
(hr : ∀ (a b : X), r a b → f a = f b)
(h : Continuous f)
:
Continuous (Quot.lift f hr)
@[deprecated isQuotientMap_quotient_mk' (since := "2024-10-22")]
Alias of isQuotientMap_quotient_mk'.
theorem
Continuous.quotient_lift
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Setoid X}
{f : X → Y}
(h : Continuous f)
(hs : ∀ (a b : X), a ≈ b → f a = f b)
:
Continuous (Quotient.lift f hs)
theorem
Continuous.quotient_liftOn'
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Setoid X}
{f : X → Y}
(h : Continuous f)
(hs : ∀ (a b : X), s a b → f a = f b)
:
Continuous fun (x : Quotient s) => x.liftOn' f hs
theorem
Continuous.quotient_map'
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Setoid X}
{t : Setoid Y}
{f : X → Y}
(hf : Continuous f)
(H : Relator.LiftFun (⇑s) (⇑t) f f)
:
Continuous (Quotient.map' f H)
theorem
continuous_pi_iff
{X : Type u}
{ι : Type u_5}
{π : ι → Type u_6}
[TopologicalSpace X]
[T : (i : ι) → TopologicalSpace (π i)]
{f : X → (i : ι) → π i}
:
theorem
continuous_pi
{X : Type u}
{ι : Type u_5}
{π : ι → Type u_6}
[TopologicalSpace X]
[T : (i : ι) → TopologicalSpace (π i)]
{f : X → (i : ι) → π i}
(h : ∀ (i : ι), Continuous fun (a : X) => f a i)
:
theorem
continuous_apply
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
(i : ι)
:
Continuous fun (p : (i : ι) → π i) => p i
theorem
continuous_apply_apply
{ι : Type u_5}
{κ : Type u_7}
{ρ : κ → ι → Type u_8}
[(j : κ) → (i : ι) → TopologicalSpace (ρ j i)]
(j : κ)
(i : ι)
:
Continuous fun (p : (j : κ) → (i : ι) → ρ j i) => p j i
theorem
continuousAt_apply
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
(i : ι)
(x : (i : ι) → π i)
:
ContinuousAt (fun (p : (i : ι) → π i) => p i) x
theorem
Continuous.piMap
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{Y : ι → Type u_8}
[(i : ι) → TopologicalSpace (Y i)]
{f : (i : ι) → π i → Y i}
(hf : ∀ (i : ι), Continuous (f i))
:
Continuous (Pi.map f)
theorem
IsOpenMap.piMap
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{Y : ι → Type u_8}
[(i : ι) → TopologicalSpace (Y i)]
{f : (i : ι) → π i → Y i}
(hfo : ∀ (i : ι), IsOpenMap (f i))
(hsurj : ∀ᶠ (i : ι) in Filter.cofinite, Function.Surjective (f i))
:
theorem
IsOpenQuotientMap.piMap
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{Y : ι → Type u_8}
[(i : ι) → TopologicalSpace (Y i)]
{f : (i : ι) → π i → Y i}
(hf : ∀ (i : ι), IsOpenQuotientMap (f i))
:
theorem
tendsto_pi_nhds
{Y : Type v}
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{f : Y → (i : ι) → π i}
{g : (i : ι) → π i}
{u : Filter Y}
:
theorem
continuousAt_pi
{X : Type u}
{ι : Type u_5}
{π : ι → Type u_6}
[TopologicalSpace X]
[T : (i : ι) → TopologicalSpace (π i)]
{f : X → (i : ι) → π i}
{x : X}
:
theorem
continuousAt_pi'
{X : Type u}
{ι : Type u_5}
{π : ι → Type u_6}
[TopologicalSpace X]
[T : (i : ι) → TopologicalSpace (π i)]
{f : X → (i : ι) → π i}
{x : X}
(hf : ∀ (i : ι), ContinuousAt (fun (y : X) => f y i) x)
:
ContinuousAt f x
theorem
ContinuousAt.piMap
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{Y : ι → Type u_8}
[(i : ι) → TopologicalSpace (Y i)]
{f : (i : ι) → π i → Y i}
{x : (i : ι) → π i}
(hf : ∀ (i : ι), ContinuousAt (f i) (x i))
:
ContinuousAt (Pi.map f) x
theorem
Pi.continuous_precomp'
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{ι' : Type u_8}
(φ : ι' → ι)
:
Continuous fun (f : (i : ι) → π i) (j : ι') => f (φ j)
theorem
Pi.continuous_precomp
{X : Type u}
{ι : Type u_5}
[TopologicalSpace X]
{ι' : Type u_8}
(φ : ι' → ι)
:
Continuous fun (x : ι → X) => x ∘ φ
theorem
Pi.continuous_postcomp'
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{X : ι → Type u_8}
[(i : ι) → TopologicalSpace (X i)]
{g : (i : ι) → π i → X i}
(hg : ∀ (i : ι), Continuous (g i))
:
Continuous fun (f : (i : ι) → π i) (i : ι) => g i (f i)
theorem
Pi.continuous_postcomp
{X : Type u}
{Y : Type v}
{ι : Type u_5}
[TopologicalSpace X]
[TopologicalSpace Y]
{g : X → Y}
(hg : Continuous g)
:
Continuous fun (x : ι → X) => g ∘ x
theorem
Pi.induced_precomp'
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{ι' : Type u_8}
(φ : ι' → ι)
:
TopologicalSpace.induced (fun (f : (i : ι) → π i) (j : ι') => f (φ j)) topologicalSpace = ⨅ (i' : ι'), TopologicalSpace.induced (Function.eval (φ i')) (T (φ i'))
theorem
Pi.induced_precomp
{Y : Type v}
{ι : Type u_5}
[TopologicalSpace Y]
{ι' : Type u_8}
(φ : ι' → ι)
:
TopologicalSpace.induced (fun (x : ι → Y) => x ∘ φ) topologicalSpace = ⨅ (i' : ι'), TopologicalSpace.induced (Function.eval (φ i')) inst✝
theorem
Pi.continuous_restrict
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
(S : Set ι)
:
theorem
Pi.continuous_restrict₂
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{s t : Set ι}
(hst : s ⊆ t)
:
Continuous (Set.restrict₂ hst)
theorem
Finset.continuous_restrict
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
(s : Finset ι)
:
theorem
Finset.continuous_restrict₂
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{s t : Finset ι}
(hst : s ⊆ t)
:
Continuous (restrict₂ hst)
theorem
Pi.continuous_restrict_apply
{X : Type u}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Z]
(s : Set X)
{f : X → Z}
(hf : Continuous f)
:
Continuous (s.restrict f)
theorem
Pi.continuous_restrict₂_apply
{X : Type u}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Z]
{s t : Set X}
(hst : s ⊆ t)
{f : ↑t → Z}
(hf : Continuous f)
:
Continuous (Set.restrict₂ hst f)
theorem
Finset.continuous_restrict_apply
{X : Type u}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Z]
(s : Finset X)
{f : X → Z}
(hf : Continuous f)
:
Continuous (s.restrict f)
theorem
Finset.continuous_restrict₂_apply
{X : Type u}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Z]
{s t : Finset X}
(hst : s ⊆ t)
{f : { x : X // x ∈ t } → Z}
(hf : Continuous f)
:
Continuous (restrict₂ hst f)
theorem
Pi.induced_restrict
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
(S : Set ι)
:
TopologicalSpace.induced S.restrict topologicalSpace = ⨅ i ∈ S, TopologicalSpace.induced (Function.eval i) (T i)
theorem
Pi.induced_restrict_sUnion
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
(𝔖 : Set (Set ι))
:
theorem
Filter.Tendsto.update
{Y : Type v}
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
[DecidableEq ι]
{l : Filter Y}
{f : Y → (i : ι) → π i}
{x : (i : ι) → π i}
(hf : Tendsto f l (nhds x))
(i : ι)
{g : Y → π i}
{xi : π i}
(hg : Tendsto g l (nhds xi))
:
Tendsto (fun (a : Y) => Function.update (f a) i (g a)) l (nhds (Function.update x i xi))
theorem
ContinuousAt.update
{X : Type u}
{ι : Type u_5}
{π : ι → Type u_6}
[TopologicalSpace X]
[T : (i : ι) → TopologicalSpace (π i)]
{f : X → (i : ι) → π i}
[DecidableEq ι]
{x : X}
(hf : ContinuousAt f x)
(i : ι)
{g : X → π i}
(hg : ContinuousAt g x)
:
ContinuousAt (fun (a : X) => Function.update (f a) i (g a)) x
theorem
Continuous.update
{X : Type u}
{ι : Type u_5}
{π : ι → Type u_6}
[TopologicalSpace X]
[T : (i : ι) → TopologicalSpace (π i)]
{f : X → (i : ι) → π i}
[DecidableEq ι]
(hf : Continuous f)
(i : ι)
{g : X → π i}
(hg : Continuous g)
:
Continuous fun (a : X) => Function.update (f a) i (g a)
theorem
continuous_update
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
[DecidableEq ι]
(i : ι)
:
Continuous fun (f : ((j : ι) → π j) × π i) => Function.update f.1 i f.2
Function.update f i x is continuous in (f, x).
theorem
continuous_mulSingle
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
[(i : ι) → One (π i)]
[DecidableEq ι]
(i : ι)
:
Continuous fun (x : π i) => Pi.mulSingle i x
Pi.mulSingle i x is continuous in x.
theorem
continuous_single
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
[(i : ι) → Zero (π i)]
[DecidableEq ι]
(i : ι)
:
Continuous fun (x : π i) => Pi.single i x
Pi.single i x is continuous in x.
theorem
ContinuousAt.finCons
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
{f : X → π 0}
{g : X → (j : Fin n) → π j.succ}
{x : X}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (fun (a : X) => Fin.cons (f a) (g a)) x
theorem
Continuous.finCons
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
{f : X → π 0}
{g : X → (j : Fin n) → π j.succ}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun (a : X) => Fin.cons (f a) (g a)
theorem
Filter.Tendsto.matrixVecCons
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace Z]
{n : ℕ}
{f : Y → Z}
{g : Y → Fin n → Z}
{l : Filter Y}
{x : Z}
{y : Fin n → Z}
(hf : Tendsto f l (nhds x))
(hg : Tendsto g l (nhds y))
:
Tendsto (fun (a : Y) => Matrix.vecCons (f a) (g a)) l (nhds (Matrix.vecCons x y))
theorem
ContinuousAt.matrixVecCons
{X : Type u}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Z]
{n : ℕ}
{f : X → Z}
{g : X → Fin n → Z}
{x : X}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (fun (a : X) => Matrix.vecCons (f a) (g a)) x
theorem
Continuous.matrixVecCons
{X : Type u}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Z]
{n : ℕ}
{f : X → Z}
{g : X → Fin n → Z}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun (a : X) => Matrix.vecCons (f a) (g a)
theorem
Filter.Tendsto.finSnoc
{Y : Type v}
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
{f : Y → (j : Fin n) → π j.castSucc}
{g : Y → π (Fin.last n)}
{l : Filter Y}
{x : (j : Fin n) → π j.castSucc}
{y : π (Fin.last n)}
(hf : Tendsto f l (nhds x))
(hg : Tendsto g l (nhds y))
:
theorem
ContinuousAt.finSnoc
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
{f : X → (j : Fin n) → π j.castSucc}
{g : X → π (Fin.last n)}
{x : X}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (fun (a : X) => Fin.snoc (f a) (g a)) x
theorem
Continuous.finSnoc
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
{f : X → (j : Fin n) → π j.castSucc}
{g : X → π (Fin.last n)}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun (a : X) => Fin.snoc (f a) (g a)
theorem
Filter.Tendsto.finInsertNth
{Y : Type v}
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
(i : Fin (n + 1))
{f : Y → π i}
{g : Y → (j : Fin n) → π (i.succAbove j)}
{l : Filter Y}
{x : π i}
{y : (j : Fin n) → π (i.succAbove j)}
(hf : Tendsto f l (nhds x))
(hg : Tendsto g l (nhds y))
:
@[deprecated Filter.Tendsto.finInsertNth (since := "2025-01-02")]
theorem
Filter.Tendsto.fin_insertNth
{Y : Type v}
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
(i : Fin (n + 1))
{f : Y → π i}
{g : Y → (j : Fin n) → π (i.succAbove j)}
{l : Filter Y}
{x : π i}
{y : (j : Fin n) → π (i.succAbove j)}
(hf : Tendsto f l (nhds x))
(hg : Tendsto g l (nhds y))
:
Alias of Filter.Tendsto.finInsertNth.
theorem
ContinuousAt.finInsertNth
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
(i : Fin (n + 1))
{f : X → π i}
{g : X → (j : Fin n) → π (i.succAbove j)}
{x : X}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (fun (a : X) => i.insertNth (f a) (g a)) x
@[deprecated ContinuousAt.finInsertNth (since := "2025-01-02")]
theorem
ContinuousAt.fin_insertNth
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
(i : Fin (n + 1))
{f : X → π i}
{g : X → (j : Fin n) → π (i.succAbove j)}
{x : X}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (fun (a : X) => i.insertNth (f a) (g a)) x
Alias of ContinuousAt.finInsertNth.
theorem
Continuous.finInsertNth
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
(i : Fin (n + 1))
{f : X → π i}
{g : X → (j : Fin n) → π (i.succAbove j)}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun (a : X) => i.insertNth (f a) (g a)
@[deprecated Continuous.finInsertNth (since := "2025-01-02")]
theorem
Continuous.fin_insertNth
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
(i : Fin (n + 1))
{f : X → π i}
{g : X → (j : Fin n) → π (i.succAbove j)}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun (a : X) => i.insertNth (f a) (g a)
Alias of Continuous.finInsertNth.
theorem
ContinuousAt.finInit
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
{f : X → (j : Fin (n + 1)) → π j}
{x : X}
(hf : ContinuousAt f x)
:
ContinuousAt (fun (a : X) => Fin.init (f a)) x
theorem
Continuous.finInit
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
{f : X → (j : Fin (n + 1)) → π j}
(hf : Continuous f)
:
Continuous fun (a : X) => Fin.init (f a)
theorem
ContinuousAt.finTail
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
{f : X → (j : Fin (n + 1)) → π j}
{x : X}
(hf : ContinuousAt f x)
:
ContinuousAt (fun (a : X) => Fin.tail (f a)) x
theorem
Continuous.finTail
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
{f : X → (j : Fin (n + 1)) → π j}
(hf : Continuous f)
:
Continuous fun (a : X) => Fin.tail (f a)
theorem
isClosed_set_pi
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{i : Set ι}
{s : (a : ι) → Set (π a)}
(hs : ∀ a ∈ i, IsClosed (s a))
:
theorem
exists_finset_piecewise_mem_of_mem_nhds
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
[DecidableEq ι]
{s : Set ((a : ι) → π a)}
{x : (a : ι) → π a}
(hs : s ∈ nhds x)
(y : (a : ι) → π a)
:
theorem
pi_eq_generateFrom
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
:
theorem
induced_to_pi
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{X : Type u_8}
(f : X → (i : ι) → π i)
:
TopologicalSpace.induced f Pi.topologicalSpace = ⨅ (i : ι), TopologicalSpace.induced (fun (x : X) => f x i) inferInstance
theorem
inducing_iInf_to_pi
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{X : Type u_8}
(f : (i : ι) → X → π i)
:
Topology.IsInducing fun (x : X) (i : ι) => f i x
Suppose π i is a family of topological spaces indexed by i : ι, and X is a type
endowed with a family of maps f i : X → π i for every i : ι, hence inducing a
map g : X → Π i, π i. This lemma shows that infimum of the topologies on X induced by
the f i as i : ι varies is simply the topology on X induced by g : X → Π i, π i
where Π i, π i is endowed with the usual product topology.
instance
Pi.discreteTopology
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
[Finite ι]
[∀ (i : ι), DiscreteTopology (π i)]
:
DiscreteTopology ((i : ι) → π i)
A finite product of discrete spaces is discrete.
theorem
continuous_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
Continuous (Sigma.mk i)
theorem
isOpenMap_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
theorem
isOpen_range_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
theorem
isClosedMap_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
IsClosedMap (Sigma.mk i)
theorem
isClosed_range_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
theorem
Topology.IsOpenEmbedding.sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
@[deprecated Topology.IsOpenEmbedding.sigmaMk (since := "2024-10-30")]
theorem
isOpenEmbedding_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
Alias of Topology.IsOpenEmbedding.sigmaMk.
@[deprecated Topology.IsOpenEmbedding.sigmaMk (since := "2024-10-18")]
theorem
openEmbedding_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
Alias of Topology.IsOpenEmbedding.sigmaMk.
theorem
Topology.IsClosedEmbedding.sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
@[deprecated Topology.IsClosedEmbedding.sigmaMk (since := "2024-10-30")]
theorem
isClosedEmbedding_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
Alias of Topology.IsClosedEmbedding.sigmaMk.
@[deprecated Topology.IsClosedEmbedding.sigmaMk (since := "2024-10-20")]
theorem
closedEmbedding_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
Alias of Topology.IsClosedEmbedding.sigmaMk.
theorem
Topology.IsEmbedding.sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
IsEmbedding (Sigma.mk i)
@[deprecated Topology.IsEmbedding.sigmaMk (since := "2024-10-26")]
theorem
embedding_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
Alias of Topology.IsEmbedding.sigmaMk.
theorem
Sigma.nhds_mk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
(i : ι)
(x : σ i)
:
theorem
Sigma.nhds_eq
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
(x : Sigma σ)
:
theorem
comap_sigmaMk_nhds
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
(i : ι)
(x : σ i)
:
theorem
isOpen_sigma_fst_preimage
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
(s : Set ι)
:
@[simp]
theorem
continuous_sigma_iff
{X : Type u}
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
[TopologicalSpace X]
{f : Sigma σ → X}
:
A map out of a sum type is continuous iff its restriction to each summand is.
theorem
continuous_sigma
{X : Type u}
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
[TopologicalSpace X]
{f : Sigma σ → X}
(hf : ∀ (i : ι), Continuous fun (a : σ i) => f ⟨i, a⟩)
:
A map out of a sum type is continuous if its restriction to each summand is.
theorem
inducing_sigma
{X : Type u}
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
[TopologicalSpace X]
{f : Sigma σ → X}
:
A map defined on a sigma type (a.k.a. the disjoint union of an indexed family of topological
spaces) is inducing iff its restriction to each component is inducing and each the image of each
component under f can be separated from the images of all other components by an open set.
@[simp]
theorem
continuous_sigma_map
{ι : Type u_5}
{κ : Type u_6}
{σ : ι → Type u_7}
{τ : κ → Type u_8}
[(i : ι) → TopologicalSpace (σ i)]
[(k : κ) → TopologicalSpace (τ k)]
{f₁ : ι → κ}
{f₂ : (i : ι) → σ i → τ (f₁ i)}
:
theorem
Continuous.sigma_map
{ι : Type u_5}
{κ : Type u_6}
{σ : ι → Type u_7}
{τ : κ → Type u_8}
[(i : ι) → TopologicalSpace (σ i)]
[(k : κ) → TopologicalSpace (τ k)]
{f₁ : ι → κ}
{f₂ : (i : ι) → σ i → τ (f₁ i)}
(hf : ∀ (i : ι), Continuous (f₂ i))
:
Continuous (Sigma.map f₁ f₂)
theorem
isOpenMap_sigma
{X : Type u}
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
[TopologicalSpace X]
{f : Sigma σ → X}
:
theorem
isOpenMap_sigma_map
{ι : Type u_5}
{κ : Type u_6}
{σ : ι → Type u_7}
{τ : κ → Type u_8}
[(i : ι) → TopologicalSpace (σ i)]
[(k : κ) → TopologicalSpace (τ k)]
{f₁ : ι → κ}
{f₂ : (i : ι) → σ i → τ (f₁ i)}
:
theorem
Topology.isInducing_sigmaMap
{ι : Type u_5}
{κ : Type u_6}
{σ : ι → Type u_7}
{τ : κ → Type u_8}
[(i : ι) → TopologicalSpace (σ i)]
[(k : κ) → TopologicalSpace (τ k)]
{f₁ : ι → κ}
{f₂ : (i : ι) → σ i → τ (f₁ i)}
(h₁ : Function.Injective f₁)
:
@[deprecated Topology.isInducing_sigmaMap (since := "2024-10-28")]
theorem
inducing_sigma_map
{ι : Type u_5}
{κ : Type u_6}
{σ : ι → Type u_7}
{τ : κ → Type u_8}
[(i : ι) → TopologicalSpace (σ i)]
[(k : κ) → TopologicalSpace (τ k)]
{f₁ : ι → κ}
{f₂ : (i : ι) → σ i → τ (f₁ i)}
(h₁ : Function.Injective f₁)
:
Alias of Topology.isInducing_sigmaMap.
theorem
Topology.isEmbedding_sigmaMap
{ι : Type u_5}
{κ : Type u_6}
{σ : ι → Type u_7}
{τ : κ → Type u_8}
[(i : ι) → TopologicalSpace (σ i)]
[(k : κ) → TopologicalSpace (τ k)]
{f₁ : ι → κ}
{f₂ : (i : ι) → σ i → τ (f₁ i)}
(h : Function.Injective f₁)
:
@[deprecated Topology.isEmbedding_sigmaMap (since := "2024-10-26")]
theorem
embedding_sigma_map
{ι : Type u_5}
{κ : Type u_6}
{σ : ι → Type u_7}
{τ : κ → Type u_8}
[(i : ι) → TopologicalSpace (σ i)]
[(k : κ) → TopologicalSpace (τ k)]
{f₁ : ι → κ}
{f₂ : (i : ι) → σ i → τ (f₁ i)}
(h : Function.Injective f₁)
:
Alias of Topology.isEmbedding_sigmaMap.
theorem
Topology.isOpenEmbedding_sigmaMap
{ι : Type u_5}
{κ : Type u_6}
{σ : ι → Type u_7}
{τ : κ → Type u_8}
[(i : ι) → TopologicalSpace (σ i)]
[(k : κ) → TopologicalSpace (τ k)]
{f₁ : ι → κ}
{f₂ : (i : ι) → σ i → τ (f₁ i)}
(h : Function.Injective f₁)
:
@[deprecated Topology.isOpenEmbedding_sigmaMap (since := "2024-10-30")]
theorem
isOpenEmbedding_sigma_map
{ι : Type u_5}
{κ : Type u_6}
{σ : ι → Type u_7}
{τ : κ → Type u_8}
[(i : ι) → TopologicalSpace (σ i)]
[(k : κ) → TopologicalSpace (τ k)]
{f₁ : ι → κ}
{f₂ : (i : ι) → σ i → τ (f₁ i)}
(h : Function.Injective f₁)
:
Alias of Topology.isOpenEmbedding_sigmaMap.
@[deprecated Topology.isOpenEmbedding_sigmaMap (since := "2024-10-18")]
theorem
openEmbedding_sigma_map
{ι : Type u_5}
{κ : Type u_6}
{σ : ι → Type u_7}
{τ : κ → Type u_8}
[(i : ι) → TopologicalSpace (σ i)]
[(k : κ) → TopologicalSpace (τ k)]
{f₁ : ι → κ}
{f₂ : (i : ι) → σ i → τ (f₁ i)}
(h : Function.Injective f₁)
:
Alias of Topology.isOpenEmbedding_sigmaMap.
@[deprecated continuous_uliftDown (since := "2025-02-10")]
Alias of continuous_uliftDown.
@[deprecated continuous_uliftUp (since := "2025-02-10")]
Alias of continuous_uliftUp.
theorem
continuous_uliftMap
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(f : X → Y)
(hf : Continuous f)
:
Continuous (ULift.map f)
@[deprecated Topology.IsEmbedding.uliftDown (since := "2024-10-26")]
Alias of Topology.IsEmbedding.uliftDown.
@[deprecated Topology.IsClosedEmbedding.uliftDown (since := "2024-10-30")]
Alias of Topology.IsClosedEmbedding.uliftDown.
@[deprecated Topology.IsClosedEmbedding.uliftDown (since := "2024-10-20")]
Alias of Topology.IsClosedEmbedding.uliftDown.
theorem
IsOpen.trans
{X : Type u}
[TopologicalSpace X]
{s : Set X}
{t : Set ↑s}
(ht : IsOpen t)
(hs : IsOpen s)
:
IsOpen (Subtype.val '' t)
theorem
IsClosed.trans
{X : Type u}
[TopologicalSpace X]
{s : Set X}
{t : Set ↑s}
(ht : IsClosed t)
(hs : IsClosed s)
:
IsClosed (Subtype.val '' t)
theorem
nhdsSet_prod_le
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(s : Set X)
(t : Set Y)
:
The product of a neighborhood of s and a neighborhood of t is a neighborhood of s ×ˢ t,
formulated in terms of a filter inequality.
theorem
Filter.eventually_nhdsSet_prod_iff
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Set X}
{t : Set Y}
{p : X × Y → Prop}
:
theorem
Filter.Eventually.prod_nhdsSet
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Set X}
{t : Set Y}
{p : X × Y → Prop}
{px : X → Prop}
{py : Y → Prop}
(hp : ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y))
(hs : ∀ᶠ (x : X) in nhdsSet s, px x)
(ht : ∀ᶠ (y : Y) in nhdsSet t, py y)
: