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
@[implicit_reducible]
instance
instTopologicalSpaceQuot
{X : Type u}
{r : X → X → Prop}
[t : TopologicalSpace X]
:
TopologicalSpace (Quot r)
@[implicit_reducible]
instance
instTopologicalSpaceQuotient
{X : Type u}
{s : Setoid X}
[t : TopologicalSpace X]
:
TopologicalSpace (Quotient s)
@[implicit_reducible]
instance
instTopologicalSpaceSigma
{ι : Type u_5}
{X : ι → Type v}
[t₂ : (i : ι) → TopologicalSpace (X i)]
:
TopologicalSpace (Sigma X)
@[implicit_reducible]
instance
Pi.topologicalSpace
{ι : Type u_5}
{Y : ι → Type v}
[t₂ : (i : ι) → TopologicalSpace (Y i)]
:
TopologicalSpace ((i : ι) → Y i)
@[implicit_reducible]
instance
ULift.topologicalSpace
{X : Type u}
[t : TopologicalSpace X]
:
TopologicalSpace (ULift.{v, u} X)
Additive, Multiplicative #
The topology on those type synonyms is inherited without change.
@[implicit_reducible]
@[implicit_reducible]
instance
instDiscreteTopologyMultiplicative
{X : Type u}
[TopologicalSpace X]
[DiscreteTopology X]
:
instance
instCompactSpaceAdditive
{X : Type u}
[TopologicalSpace X]
[CompactSpace X]
:
CompactSpace (Additive X)
instance
instWeaklyLocallyCompactSpaceAdditive
{X : Type u}
[TopologicalSpace X]
[WeaklyLocallyCompactSpace X]
:
instance
instWeaklyLocallyCompactSpaceMultiplicative
{X : Type u}
[TopologicalSpace X]
[WeaklyLocallyCompactSpace X]
:
instance
instLocallyCompactSpaceAdditive
{X : Type u}
[TopologicalSpace X]
[LocallyCompactSpace X]
:
instance
instLocallyCompactSpaceMultiplicative
{X : Type u}
[TopologicalSpace X]
[LocallyCompactSpace X]
:
theorem
nhds_ofMul
{X : Type u}
[TopologicalSpace X]
(x : X)
:
nhds (Additive.ofMul x) = Filter.map (⇑Additive.ofMul) (nhds x)
theorem
nhds_ofAdd
{X : Type u}
[TopologicalSpace X]
(x : X)
:
nhds (Multiplicative.ofAdd x) = Filter.map (⇑Multiplicative.ofAdd) (nhds x)
theorem
nhds_toMul
{X : Type u}
[TopologicalSpace X]
(x : Additive X)
:
nhds (Additive.toMul x) = Filter.map (⇑Additive.toMul) (nhds x)
theorem
nhds_toAdd
{X : Type u}
[TopologicalSpace X]
(x : Multiplicative X)
:
nhds (Multiplicative.toAdd x) = Filter.map (⇑Multiplicative.toAdd) (nhds x)
Order dual #
The topology on this type synonym is inherited without change.
@[implicit_reducible]
theorem
nhds_toDual
{X : Type u}
[TopologicalSpace X]
(x : X)
:
nhds (OrderDual.toDual x) = Filter.map (⇑OrderDual.toDual) (nhds x)
theorem
nhds_ofDual
{X : Type u}
[TopologicalSpace X]
(x : X)
:
nhds (OrderDual.ofDual x) = Filter.map (⇑OrderDual.ofDual) (nhds x)
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))
:
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]
:
DiscreteTopology (Subtype p)
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)]
:
DiscreteTopology (Sigma Y)
@[simp]
theorem
comap_nhdsWithin_range
{α : Type u_5}
{β : Type u_6}
[TopologicalSpace β]
(f : α → β)
(y : β)
:
Filter.comap f (nhdsWithin y (Set.range f)) = Filter.comap f (nhds y)
theorem
mem_nhds_subtype
{X : Type u}
[TopologicalSpace X]
(s : Set X)
(x : { x : X // x ∈ s })
(t : Set { x : X // x ∈ s })
:
theorem
nhds_subtype
{X : Type u}
[TopologicalSpace X]
(s : Set X)
(x : { x : X // x ∈ s })
:
nhds x = Filter.comap Subtype.val (nhds ↑x)
theorem
nhds_subtype_eq_comap_nhdsWithin
{X : Type u}
[TopologicalSpace X]
(s : Set X)
(x : { x : X // x ∈ s })
:
nhds x = Filter.comap Subtype.val (nhdsWithin (↑x) s)
theorem
nhdsWithin_subtype_eq_bot_iff
{X : Type u}
[TopologicalSpace X]
{s t : Set X}
{x : ↑s}
:
nhdsWithin x (Subtype.val ⁻¹' t) = ⊥ ↔ nhdsWithin (↑x) t ⊓ Filter.principal s = ⊥
theorem
nhds_ne_subtype_eq_bot_iff
{X : Type u}
[TopologicalSpace X]
{S : Set X}
{x : ↑S}
:
nhdsWithin x {x}ᶜ = ⊥ ↔ nhdsWithin ↑x {↑x}ᶜ ⊓ Filter.principal S = ⊥
theorem
nhds_ne_subtype_neBot_iff
{X : Type u}
[TopologicalSpace X]
{S : Set X}
{x : ↑S}
:
(nhdsWithin x {x}ᶜ).NeBot ↔ (nhdsWithin ↑x {↑x}ᶜ ⊓ Filter.principal S).NeBot
A subset s is discrete if the corresponding subtype (with the subspace topology) is a
discrete space.
- to_subtype : DiscreteTopology ↑s
Instances For
theorem
isDiscrete_iff_discreteTopology
{X : Type u_5}
[TopologicalSpace X]
{s : Set X}
:
IsDiscrete s ↔ DiscreteTopology ↑s
theorem
SetLike.isDiscrete_iff_discreteTopology
{X : Type u_5}
[TopologicalSpace X]
{S : Type u_6}
[SetLike S X]
{s : S}
:
IsDiscrete ↑s ↔ DiscreteTopology ↥s
theorem
DiscreteTopology.isDiscrete
{X : Type u_5}
[TopologicalSpace X]
{s : Set X}
[DiscreteTopology ↑s]
:
A type synonym equipped with the topology whose open sets are the empty set and the sets with finite complements.
Instances For
The identity equivalence between X and CofiniteTopology X.
Instances For
@[implicit_reducible]
@[implicit_reducible]
theorem
CofiniteTopology.nhds_eq
{X : Type u}
(x : CofiniteTopology X)
:
nhds x = pure x ⊔ Filter.cofinite
theorem
CofiniteTopology.mem_nhds_iff
{X : Type u}
{x : CofiniteTopology X}
{s : Set (CofiniteTopology X)}
:
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)
:
MapClusterPt (x, y) (la.curry lb) (Prod.map f 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)
:
MapClusterPt (x, y) (la ×ˢ lb) (Prod.map f g)
theorem
continuous_bool_rng
{X : Type u}
[TopologicalSpace X]
{f : X → Bool}
(b : Bool)
:
Continuous f ↔ IsClopen (f ⁻¹' {b})
theorem
Topology.IsInducing.subtypeVal
{Y : Type v}
[TopologicalSpace Y]
{t : Set Y}
:
IsInducing Subtype.val
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))
:
theorem
Topology.IsEmbedding.subtypeVal
{X : Type u}
[TopologicalSpace X]
{p : X → Prop}
:
IsEmbedding Subtype.val
theorem
Topology.IsClosedEmbedding.subtypeVal
{X : Type u}
[TopologicalSpace X]
{p : X → Prop}
(h : IsClosed {a : X | p a})
:
IsClosedEmbedding Subtype.val
theorem
continuous_subtype_val
{X : Type u}
[TopologicalSpace X]
{p : X → Prop}
:
Continuous Subtype.val
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)
:
Topology.IsOpenEmbedding Subtype.val
theorem
IsOpen.isOpenMap_subtype_val
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(hs : IsOpen s)
:
IsOpenMap Subtype.val
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)
:
Topology.IsClosedEmbedding Subtype.val
theorem
IsClosed.isClosedMap_subtype_val
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(hs : IsClosed s)
:
IsClosedMap Subtype.val
theorem
IsClosedMap.restrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : IsClosedMap f)
{s : Set X}
(hs : IsClosed s)
:
IsClosedMap (s.restrict f)
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
IsOpenMap.subtype_mk
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{p : X → Prop}
{f : Y → X}
(hf : IsOpenMap f)
(hp : ∀ (x : Y), p (f x))
:
IsOpenMap fun (x : Y) => ⟨f x, ⋯⟩
theorem
IsClosedMap.subtype_mk
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{p : X → Prop}
{f : Y → X}
(hf : IsClosedMap f)
(hp : ∀ (x : Y), p (f x))
:
IsClosedMap fun (x : Y) => ⟨f x, ⋯⟩
theorem
Continuous.subtype_coind
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{p : X → Prop}
{f : Y → X}
(hf : Continuous f)
(hp : ∀ (x : Y), p (f x))
:
Continuous (Subtype.coind f hp)
theorem
IsOpenMap.subtype_coind
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{p : X → Prop}
{f : Y → X}
(hf : IsOpenMap f)
(hp : ∀ (x : Y), p (f x))
:
IsOpenMap (Subtype.coind f hp)
theorem
IsClosedMap.subtype_coind
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{p : X → Prop}
{f : Y → X}
(hf : IsClosedMap f)
(hp : ∀ (x : Y), p (f x))
:
IsClosedMap (Subtype.coind f hp)
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
IsOpenMap.subtype_map
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : IsOpenMap f)
{s : Set X}
{t : Set Y}
(hs : IsOpen s)
(hst : ∀ x ∈ s, f x ∈ t)
:
IsOpenMap (Subtype.map f hst)
theorem
IsClosedMap.subtype_map
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : IsClosedMap f)
{s : Set X}
{t : Set Y}
(hs : IsClosed s)
(hst : ∀ x ∈ s, f x ∈ t)
:
IsClosedMap (Subtype.map f hst)
theorem
IsOpen.isOpenMap_inclusion
{X : Type u}
[TopologicalSpace X]
{s t : Set X}
(hs : IsOpen s)
(h : s ⊆ t)
:
theorem
IsClosed.isClosedMap_inclusion
{X : Type u}
[TopologicalSpace X]
{s t : Set X}
(hs : IsClosed s)
(h : s ⊆ t)
:
@[simp]
theorem
continuous_rangeFactorization_iff
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
:
theorem
Continuous.rangeFactorization
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : Continuous f)
:
theorem
continuousAt_subtype_val
{X : Type u}
[TopologicalSpace X]
{p : X → Prop}
{x : Subtype p}
:
ContinuousAt Subtype.val x
The induced homeomorphism between two equal subtypes of a given topological space:
the underlying equivalence is Equiv.subtypeEquivProp.
Instances For
@[simp]
theorem
Homeomorph.ofEqSubtypes_toEquiv
{X : Type u}
[TopologicalSpace X]
{p q : X → Prop}
(hpq : p = q)
:
(ofEqSubtypes hpq).toEquiv = Equiv.subtypeEquivProp hpq
@[simp]
theorem
denseRange_inclusion_iff
{X : Type u}
[TopologicalSpace X]
{s t : Set X}
(hst : s ⊆ t)
:
DenseRange (Set.inclusion hst) ↔ t ⊆ closure s
theorem
map_nhds_subtype_val
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(x : ↑s)
:
Filter.map Subtype.val (nhds x) = nhdsWithin (↑x) s
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)
:
Filter.map Subtype.val (nhds ⟨x, hx⟩) = nhds x
theorem
nhds_subtype_eq_comap
{X : Type u}
[TopologicalSpace X]
{p : X → Prop}
{x : X}
{h : p x}
:
nhds ⟨x, h⟩ = Filter.comap Subtype.val (nhds 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}
:
Filter.Tendsto f l (nhds x) ↔ Filter.Tendsto (fun (x : Y) => ↑(f x)) l (nhds ↑x)
theorem
closure_subtype
{X : Type u}
[TopologicalSpace X]
{p : X → Prop}
{x : { a : X // p a }}
{s : Set { a : X // p a }}
:
@[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}
:
ContinuousAt (Set.codRestrict f t h1) x ↔ ContinuousAt f 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
IsOpenMap.codRestrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : IsOpenMap f)
{s : Set Y}
(hs : ∀ (a : X), f a ∈ s)
:
IsOpenMap (Set.codRestrict f s hs)
theorem
IsClosedMap.codRestrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : IsClosedMap f)
{s : Set Y}
(hs : ∀ (a : X), f a ∈ s)
:
IsClosedMap (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
IsOpenMap.mapsToRestrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : IsOpenMap f)
{s : Set X}
{t : Set Y}
(hs : IsOpen s)
(ht : Set.MapsTo f s t)
:
IsOpenMap (Set.MapsTo.restrict f s t ht)
theorem
IsClosedMap.mapsToRestrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : IsClosedMap f)
{s : Set X}
{t : Set Y}
(hs : IsClosed s)
(ht : Set.MapsTo f s t)
:
IsClosedMap (Set.MapsTo.restrict f s t ht)
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.IsEmbedding.restrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : IsEmbedding f)
{s : Set X}
{t : Set Y}
(H : Set.MapsTo f s t)
:
IsEmbedding (Set.MapsTo.restrict f s t H)
theorem
Topology.IsOpenEmbedding.restrict
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : IsOpenEmbedding f)
{s : Set X}
{t : Set Y}
(H : Set.MapsTo f s t)
(hs : IsOpen s)
:
IsOpenEmbedding (Set.MapsTo.restrict f s t H)
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)
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)
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))
:
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 X on s is discrete, then also the topology induces on t is discrete.
(Compare IsDiscrete.mono which is the same thing stated without using subtypes.)
theorem
IsDiscrete.mono
{X : Type u}
[TopologicalSpace X]
{s t : Set X}
(hs : IsDiscrete s)
(hst : t ⊆ s)
:
Let s, t ⊆ X be two subsets of a topological space X. If t ⊆ s and s is discrete,
then t is discrete.
(Compare DiscreteTopology.of_subset which is the same thing stated in terms of subtypes.)
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.
theorem
exists_open_dense_of_open_dense_subtype
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(hs : Dense s)
{u : Set ↑s}
(huo : IsOpen u)
(hud : Dense u)
:
If s is dense in X and u is open and dense in s, then u = v ∩ s for some v that is
open and dense in X.
@[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)
:
theorem
isQuotientMap_quot_mk
{X : Type u}
[TopologicalSpace X]
{r : X → X → Prop}
:
Topology.IsQuotientMap (Quot.mk r)
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)
theorem
isQuotientMap_quotient_mk'
{X : Type u}
[TopologicalSpace X]
{s : Setoid X}
:
Topology.IsQuotientMap Quotient.mk'
theorem
continuous_quotient_mk'
{X : Type u}
[TopologicalSpace X]
{s : Setoid X}
:
Continuous 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}
{A : ι → Type u_6}
[TopologicalSpace X]
[T : (i : ι) → TopologicalSpace (A i)]
{f : X → (i : ι) → A i}
:
Continuous f ↔ ∀ (i : ι), Continuous fun (a : X) => f a i
theorem
continuous_pi
{X : Type u}
{ι : Type u_5}
{A : ι → Type u_6}
[TopologicalSpace X]
[T : (i : ι) → TopologicalSpace (A i)]
{f : X → (i : ι) → A i}
(h : ∀ (i : ι), Continuous fun (a : X) => f a i)
:
theorem
continuous_apply
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
(i : ι)
:
Continuous fun (p : (i : ι) → A i) => p i
theorem
continuous_apply_apply
{ι : Type u_5}
{κ : Type u_8}
{ρ : κ → ι → Type u_9}
[(j : κ) → (i : ι) → TopologicalSpace (ρ j i)]
(j : κ)
(i : ι)
:
Continuous fun (p : (j : κ) → (i : ι) → ρ j i) => p j i
theorem
continuousAt_apply
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
(i : ι)
(x : (i : ι) → A i)
:
ContinuousAt (fun (p : (i : ι) → A i) => p i) x
theorem
Filter.Tendsto.apply_nhds
{Y : Type v}
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
{l : Filter Y}
{f : Y → (i : ι) → A i}
{x : (i : ι) → A i}
(h : Tendsto f l (nhds x))
(i : ι)
:
theorem
Continuous.piMap
{ι : Type u_5}
{A : ι → Type u_6}
{B : ι → Type u_7}
[T : (i : ι) → TopologicalSpace (A i)]
[(i : ι) → TopologicalSpace (B i)]
{f : (i : ι) → A i → B i}
(hf : ∀ (i : ι), Continuous (f i))
:
Continuous (Pi.map f)
theorem
IsOpenMap.piMap
{ι : Type u_5}
{A : ι → Type u_6}
{B : ι → Type u_7}
[T : (i : ι) → TopologicalSpace (A i)]
[(i : ι) → TopologicalSpace (B i)]
{f : (i : ι) → A i → B i}
(hfo : ∀ (i : ι), IsOpenMap (f i))
(hsurj : ∀ᶠ (i : ι) in Filter.cofinite, Function.Surjective (f i))
:
theorem
IsOpenQuotientMap.piMap
{ι : Type u_5}
{A : ι → Type u_6}
{B : ι → Type u_7}
[T : (i : ι) → TopologicalSpace (A i)]
[(i : ι) → TopologicalSpace (B i)]
{f : (i : ι) → A i → B i}
(hf : ∀ (i : ι), IsOpenQuotientMap (f i))
:
theorem
tendsto_pi_nhds
{Y : Type v}
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
{f : Y → (i : ι) → A i}
{g : (i : ι) → A i}
{u : Filter Y}
:
Filter.Tendsto f u (nhds g) ↔ ∀ (x : ι), Filter.Tendsto (fun (i : Y) => f i x) u (nhds (g x))
theorem
continuousAt_pi
{X : Type u}
{ι : Type u_5}
{A : ι → Type u_6}
[TopologicalSpace X]
[T : (i : ι) → TopologicalSpace (A i)]
{f : X → (i : ι) → A i}
{x : X}
:
ContinuousAt f x ↔ ∀ (i : ι), ContinuousAt (fun (y : X) => f y i) x
theorem
continuousAt_pi'
{X : Type u}
{ι : Type u_5}
{A : ι → Type u_6}
[TopologicalSpace X]
[T : (i : ι) → TopologicalSpace (A i)]
{f : X → (i : ι) → A i}
{x : X}
(hf : ∀ (i : ι), ContinuousAt (fun (y : X) => f y i) x)
:
ContinuousAt f x
theorem
ContinuousAt.piMap
{ι : Type u_5}
{A : ι → Type u_6}
{B : ι → Type u_7}
[T : (i : ι) → TopologicalSpace (A i)]
[(i : ι) → TopologicalSpace (B i)]
{f : (i : ι) → A i → B i}
{x : (i : ι) → A i}
(hf : ∀ (i : ι), ContinuousAt (f i) (x i))
:
ContinuousAt (Pi.map f) x
theorem
Topology.IsInducing.piMap
{ι : Type u_5}
{A : ι → Type u_6}
{B : ι → Type u_7}
[T : (i : ι) → TopologicalSpace (A i)]
[(i : ι) → TopologicalSpace (B i)]
{f : (i : ι) → A i → B i}
(hf : ∀ (i : ι), IsInducing (f i))
:
IsInducing (Pi.map f)
theorem
Topology.IsEmbedding.piMap
{ι : Type u_5}
{A : ι → Type u_6}
{B : ι → Type u_7}
[T : (i : ι) → TopologicalSpace (A i)]
[(i : ι) → TopologicalSpace (B i)]
{f : (i : ι) → A i → B i}
(hf : ∀ (i : ι), IsEmbedding (f i))
:
IsEmbedding (Pi.map f)
theorem
Pi.continuous_precomp'
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
{ι' : Type u_9}
(φ : ι' → ι)
:
Continuous fun (f : (i : ι) → A i) (j : ι') => f (φ j)
theorem
Pi.continuous_precomp
{X : Type u}
{ι : Type u_5}
[TopologicalSpace X]
{ι' : Type u_9}
(φ : ι' → ι)
:
Continuous fun (x : ι → X) => x ∘ φ
theorem
Pi.continuous_postcomp'
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
{X : ι → Type u_9}
[(i : ι) → TopologicalSpace (X i)]
{g : (i : ι) → A i → X i}
(hg : ∀ (i : ι), Continuous (g i))
:
Continuous fun (f : (i : ι) → A 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}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
{ι' : Type u_9}
(φ : ι' → ι)
:
TopologicalSpace.induced (fun (f : (i : ι) → A 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_9}
(φ : ι' → ι)
:
TopologicalSpace.induced (fun (x : ι → Y) => x ∘ φ) topologicalSpace = ⨅ (i' : ι'), TopologicalSpace.induced (Function.eval (φ i')) inst✝
Homeomorphism between X → Y → Z and X × Y → Z with product topologies.
Instances For
@[simp]
theorem
Homeomorph.piCurry_symm_apply
{X : Type u_9}
{Y : Type u_10}
{Z : Type u_11}
[TopologicalSpace Z]
(a✝ : X → Y → Z)
(a✝¹ : X × Y)
:
@[simp]
theorem
Homeomorph.piCurry_apply
{X : Type u_9}
{Y : Type u_10}
{Z : Type u_11}
[TopologicalSpace Z]
(a✝ : X × Y → Z)
(a✝¹ : X)
(a✝² : Y)
:
piCurry a✝ a✝¹ a✝² = Function.curry a✝ a✝¹ a✝²
theorem
Pi.continuous_restrict
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
(S : Set ι)
:
theorem
Pi.continuous_restrict₂
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
{s t : Set ι}
(hst : s ⊆ t)
:
Continuous (Set.restrict₂ hst)
theorem
Finset.continuous_restrict
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
(s : Finset ι)
:
theorem
Finset.continuous_restrict₂
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A 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 : ↥t → Z}
(hf : Continuous f)
:
Continuous (restrict₂ hst f)
theorem
Pi.induced_restrict
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A 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}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
(𝔖 : Set (Set ι))
:
theorem
Filter.Tendsto.update
{Y : Type v}
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
[DecidableEq ι]
{l : Filter Y}
{f : Y → (i : ι) → A i}
{x : (i : ι) → A i}
(hf : Tendsto f l (nhds x))
(i : ι)
{g : Y → A i}
{xi : A 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}
{A : ι → Type u_6}
[TopologicalSpace X]
[T : (i : ι) → TopologicalSpace (A i)]
{f : X → (i : ι) → A i}
[DecidableEq ι]
{x : X}
(hf : ContinuousAt f x)
(i : ι)
{g : X → A 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}
{A : ι → Type u_6}
[TopologicalSpace X]
[T : (i : ι) → TopologicalSpace (A i)]
{f : X → (i : ι) → A i}
[DecidableEq ι]
(hf : Continuous f)
(i : ι)
{g : X → A i}
(hg : Continuous g)
:
Continuous fun (a : X) => Function.update (f a) i (g a)
theorem
continuous_update
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
[DecidableEq ι]
(i : ι)
:
Continuous fun (f : ((j : ι) → A j) × A i) => Function.update f.1 i f.2
Function.update f i x is continuous in (f, x).
theorem
continuous_mulSingle
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
[(i : ι) → One (A i)]
[DecidableEq ι]
(i : ι)
:
Continuous fun (x : A i) => Pi.mulSingle i x
Pi.mulSingle i x is continuous in x.
theorem
continuous_single
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
[(i : ι) → Zero (A i)]
[DecidableEq ι]
(i : ι)
:
Continuous fun (x : A i) => Pi.single i x
Pi.single i x is continuous in x.
theorem
Filter.Tendsto.finCons
{Y : Type v}
{n : ℕ}
{A : Fin (n + 1) → Type u_9}
[(i : Fin (n + 1)) → TopologicalSpace (A i)]
{f : Y → A 0}
{g : Y → (j : Fin n) → A j.succ}
{l : Filter Y}
{x : A 0}
{y : (j : Fin n) → A j.succ}
(hf : Tendsto f l (nhds x))
(hg : Tendsto g l (nhds y))
:
theorem
ContinuousAt.finCons
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{A : Fin (n + 1) → Type u_9}
[(i : Fin (n + 1)) → TopologicalSpace (A i)]
{f : X → A 0}
{g : X → (j : Fin n) → A 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 : ℕ}
{A : Fin (n + 1) → Type u_9}
[(i : Fin (n + 1)) → TopologicalSpace (A i)]
{f : X → A 0}
{g : X → (j : Fin n) → A 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 : ℕ}
{A : Fin (n + 1) → Type u_9}
[(i : Fin (n + 1)) → TopologicalSpace (A i)]
{f : Y → (j : Fin n) → A j.castSucc}
{g : Y → A (Fin.last n)}
{l : Filter Y}
{x : (j : Fin n) → A j.castSucc}
{y : A (Fin.last n)}
(hf : Tendsto f l (nhds x))
(hg : Tendsto g l (nhds y))
:
theorem
ContinuousAt.finSnoc
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{A : Fin (n + 1) → Type u_9}
[(i : Fin (n + 1)) → TopologicalSpace (A i)]
{f : X → (j : Fin n) → A j.castSucc}
{g : X → A (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 : ℕ}
{A : Fin (n + 1) → Type u_9}
[(i : Fin (n + 1)) → TopologicalSpace (A i)]
{f : X → (j : Fin n) → A j.castSucc}
{g : X → A (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 : ℕ}
{A : Fin (n + 1) → Type u_9}
[(i : Fin (n + 1)) → TopologicalSpace (A i)]
(i : Fin (n + 1))
{f : Y → A i}
{g : Y → (j : Fin n) → A (i.succAbove j)}
{l : Filter Y}
{x : A i}
{y : (j : Fin n) → A (i.succAbove j)}
(hf : Tendsto f l (nhds x))
(hg : Tendsto g l (nhds y))
:
theorem
ContinuousAt.finInsertNth
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{A : Fin (n + 1) → Type u_9}
[(i : Fin (n + 1)) → TopologicalSpace (A i)]
(i : Fin (n + 1))
{f : X → A i}
{g : X → (j : Fin n) → A (i.succAbove j)}
{x : X}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (fun (a : X) => i.insertNth (f a) (g a)) x
theorem
Continuous.finInsertNth
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{A : Fin (n + 1) → Type u_9}
[(i : Fin (n + 1)) → TopologicalSpace (A i)]
(i : Fin (n + 1))
{f : X → A i}
{g : X → (j : Fin n) → A (i.succAbove j)}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun (a : X) => i.insertNth (f a) (g a)
theorem
ContinuousAt.finInit
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{A : Fin (n + 1) → Type u_9}
[(i : Fin (n + 1)) → TopologicalSpace (A i)]
{f : X → (j : Fin (n + 1)) → A 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 : ℕ}
{A : Fin (n + 1) → Type u_9}
[(i : Fin (n + 1)) → TopologicalSpace (A i)]
{f : X → (j : Fin (n + 1)) → A j}
(hf : Continuous f)
:
Continuous fun (a : X) => Fin.init (f a)
theorem
ContinuousAt.finTail
{X : Type u}
[TopologicalSpace X]
{n : ℕ}
{A : Fin (n + 1) → Type u_9}
[(i : Fin (n + 1)) → TopologicalSpace (A i)]
{f : X → (j : Fin (n + 1)) → A 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 : ℕ}
{A : Fin (n + 1) → Type u_9}
[(i : Fin (n + 1)) → TopologicalSpace (A i)]
{f : X → (j : Fin (n + 1)) → A j}
(hf : Continuous f)
:
Continuous fun (a : X) => Fin.tail (f a)
theorem
isOpen_set_pi
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
{i : Set ι}
{s : (a : ι) → Set (A a)}
(hi : i.Finite)
(hs : ∀ a ∈ i, IsOpen (s a))
:
theorem
isOpen_pi_iff
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
{s : Set ((a : ι) → A a)}
:
theorem
isClosed_set_pi
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
{i : Set ι}
{s : (a : ι) → Set (A a)}
(hs : ∀ a ∈ i, IsClosed (s a))
:
theorem
Topology.IsClosedEmbedding.piMap
{ι : Type u_5}
{A : ι → Type u_6}
{B : ι → Type u_7}
[T : (i : ι) → TopologicalSpace (A i)]
[(i : ι) → TopologicalSpace (B i)]
{f : (i : ι) → A i → B i}
(hf : ∀ (i : ι), IsClosedEmbedding (f i))
:
theorem
Topology.IsOpenEmbedding.piMap
{ι : Type u_5}
{A : ι → Type u_6}
{B : ι → Type u_7}
[T : (i : ι) → TopologicalSpace (A i)]
[(i : ι) → TopologicalSpace (B i)]
[Finite ι]
{f : (i : ι) → A i → B i}
(hf : ∀ (i : ι), IsOpenEmbedding (f i))
:
theorem
mem_nhds_of_pi_mem_nhds
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
{I : Set ι}
{s : (i : ι) → Set (A i)}
(a : (i : ι) → A i)
(hs : I.pi s ∈ nhds a)
{i : ι}
(hi : i ∈ I)
:
s i ∈ nhds (a i)
theorem
set_pi_mem_nhds
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
{i : Set ι}
{s : (a : ι) → Set (A a)}
{x : (a : ι) → A a}
(hi : i.Finite)
(hs : ∀ a ∈ i, s a ∈ nhds (x a))
:
theorem
set_pi_mem_nhds_iff
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
{I : Set ι}
(hI : I.Finite)
{s : (i : ι) → Set (A i)}
(a : (i : ι) → A i)
:
theorem
exists_finset_piecewise_mem_of_mem_nhds
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
[DecidableEq ι]
{s : Set ((a : ι) → A a)}
{x : (a : ι) → A a}
(hs : s ∈ nhds x)
(y : (a : ι) → A a)
:
theorem
pi_generateFrom_eq
{ι : Type u_5}
{A : ι → Type u_9}
{g : (a : ι) → Set (Set (A a))}
:
Pi.topologicalSpace = TopologicalSpace.generateFrom
{t : Set ((i : ι) → A i) | ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}
theorem
pi_eq_generateFrom
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
:
theorem
induced_to_pi
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
{X : Type u_9}
(f : X → (i : ι) → A i)
:
TopologicalSpace.induced f Pi.topologicalSpace = ⨅ (i : ι), TopologicalSpace.induced (fun (x : X) => f x i) inferInstance
theorem
inducing_iInf_to_pi
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
{X : Type u_9}
(f : (i : ι) → X → A i)
:
Topology.IsInducing fun (x : X) (i : ι) => f i x
Suppose A i is a family of topological spaces indexed by i : ι, and X is a type
endowed with a family of maps f i : X → A i for every i : ι, hence inducing a
map g : X → Π i, A 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, A i
where Π i, A i is endowed with the usual product topology.
instance
Pi.discreteTopology
{ι : Type u_5}
{A : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (A i)]
[Finite ι]
[∀ (i : ι), DiscreteTopology (A i)]
:
DiscreteTopology ((i : ι) → A i)
A finite product of discrete spaces is discrete.
theorem
Function.Surjective.isEmbedding_comp
{X : Type u}
[TopologicalSpace X]
{n : Type u_9}
{m : Type u_10}
(f : m → n)
(hf : Surjective f)
:
Topology.IsEmbedding fun (x : n → X) => x ∘ f
theorem
continuous_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
Continuous (Sigma.mk i)
theorem
isOpen_sigma_iff
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{s : Set (Sigma σ)}
:
theorem
isClosed_sigma_iff
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{s : Set (Sigma σ)}
:
theorem
isOpenMap_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
IsOpenMap (Sigma.mk 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 : ι}
:
IsOpenEmbedding (Sigma.mk i)
theorem
Topology.IsClosedEmbedding.sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
IsClosedEmbedding (Sigma.mk i)
theorem
Topology.IsEmbedding.sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
IsEmbedding (Sigma.mk i)
theorem
Sigma.nhds_mk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
(i : ι)
(x : σ i)
:
nhds ⟨i, x⟩ = Filter.map (mk i) (nhds x)
theorem
Sigma.nhds_eq
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
(x : Sigma σ)
:
nhds x = Filter.map (mk x.fst) (nhds x.snd)
theorem
comap_sigmaMk_nhds
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
(i : ι)
(x : σ i)
:
Filter.comap (Sigma.mk i) (nhds ⟨i, x⟩) = nhds x
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}
:
Continuous f ↔ ∀ (i : ι), Continuous fun (a : σ i) => f ⟨i, a⟩
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}
:
Topology.IsInducing f ↔ (∀ (i : ι), Topology.IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ (U : Set X), IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
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)}
:
Continuous (Sigma.map f₁ f₂) ↔ ∀ (i : ι), Continuous (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₁)
:
IsInducing (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsInducing (f₂ i)
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₁)
:
IsEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsEmbedding (f₂ i)
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₁)
:
IsOpenEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsOpenEmbedding (f₂ i)
theorem
continuous_uliftMap
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(f : X → Y)
(hf : Continuous f)
:
Continuous (ULift.map f)
theorem
Topology.IsClosedEmbedding.uliftDown
{X : Type u}
[TopologicalSpace X]
:
IsClosedEmbedding ULift.down
instance
instDiscreteTopologyULift
{X : Type u}
[TopologicalSpace X]
[DiscreteTopology X]
:
DiscreteTopology (ULift.{u_5, u} X)
Continuous maps between ULift X and ULift Y are equivalent to continuous maps between X
and Y.
Instances For
@[simp]
theorem
ContinuousMap.uliftEquiv_apply_apply
(X : Type u)
(Y : Type v)
[TopologicalSpace X]
[TopologicalSpace Y]
(f : C(ULift.{v, u} X, ULift.{u, v} Y))
(a✝ : X)
:
((uliftEquiv X Y) f) a✝ = (ULift.down ∘ ⇑f ∘ ULift.up) a✝
@[simp]
theorem
ContinuousMap.uliftEquiv_symm_apply_apply
(X : Type u)
(Y : Type v)
[TopologicalSpace X]
[TopologicalSpace Y]
(f : C(X, Y))
(a✝ : ULift.{v, u} X)
:
((uliftEquiv X Y).symm f) a✝ = (ULift.up ∘ ⇑f ∘ ULift.down) a✝
theorem
IsOpen.trans
{X : Type u}
[TopologicalSpace X]
{s : Set X}
{t : Set ↑s}
(ht : IsOpen t)
(hs : IsOpen s)
:
theorem
IsClosed.trans
{X : Type u}
[TopologicalSpace X]
{s : Set X}
{t : Set ↑s}
(ht : IsClosed t)
(hs : IsClosed s)
:
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)
: