Constructions of new topological spaces from old ones #
This file constructs products, sums, 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, sum, disjoint union, subspace, quotient space
instance
instTopologicalSpaceQuot
{X : Type u}
{r : X → X → Prop}
[t : TopologicalSpace X]
:
TopologicalSpace (Quot r)
Equations
- instTopologicalSpaceQuot = TopologicalSpace.coinduced (Quot.mk r) t
Equations
- instTopologicalSpaceQuotient = TopologicalSpace.coinduced Quotient.mk' t
instance
instTopologicalSpaceProd
{X : Type u}
{Y : Type v}
[t₁ : TopologicalSpace X]
[t₂ : TopologicalSpace Y]
:
TopologicalSpace (X × Y)
Equations
- instTopologicalSpaceProd = TopologicalSpace.induced Prod.fst t₁ ⊓ TopologicalSpace.induced Prod.snd t₂
instance
instTopologicalSpaceSum
{X : Type u}
{Y : Type v}
[t₁ : TopologicalSpace X]
[t₂ : TopologicalSpace Y]
:
TopologicalSpace (X ⊕ Y)
Equations
- instTopologicalSpaceSum = TopologicalSpace.coinduced Sum.inl t₁ ⊔ TopologicalSpace.coinduced Sum.inr t₂
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)
Equations
- ULift.topologicalSpace = TopologicalSpace.induced ULift.down t
Additive, Multiplicative #
The topology on those type synonyms is inherited without change.
Equations
- instTopologicalSpaceAdditive = inst
Equations
- instTopologicalSpaceMultiplicative = inst
Equations
- ⋯ = inst
instance
instDiscreteTopologyMultiplicative
{X : Type u}
[TopologicalSpace X]
[DiscreteTopology X]
:
Equations
- ⋯ = inst
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.
Equations
- OrderDual.instTopologicalSpace = inst
Equations
- ⋯ = inst
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 (OrderDual.toDual x) (Set.Ioi (OrderDual.toDual x))).NeBot
Equations
- ⋯ = inst
instance
OrderDual.instNeBotNhdsWithinIio
{X : Type u}
[TopologicalSpace X]
[Preorder X]
{x : X}
[(nhdsWithin x (Set.Ioi x)).NeBot]
:
(nhdsWithin (OrderDual.toDual x) (Set.Iio (OrderDual.toDual x))).NeBot
Equations
- ⋯ = inst
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_of_le
{α : Type u_5}
[TopologicalSpace α]
{s : Setoid α}
{t : Setoid α}
(h : s ≤ t)
:
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]
:
Equations
- ⋯ = ⋯
instance
Sum.discreteTopology
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
[h : DiscreteTopology X]
[hY : DiscreteTopology Y]
:
DiscreteTopology (X ⊕ Y)
Equations
- ⋯ = ⋯
instance
Sigma.discreteTopology
{ι : Type u_5}
{Y : ι → Type v}
[(i : ι) → TopologicalSpace (Y i)]
[h : ∀ (i : ι), DiscreteTopology (Y i)]
:
Equations
- ⋯ = ⋯
@[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
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 : Set X}
{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
theorem
discreteTopology_subtype_iff
{X : Type u}
[TopologicalSpace X]
{S : Set X}
:
DiscreteTopology ↑S ↔ ∀ x ∈ S, nhdsWithin x {x}ᶜ ⊓ Filter.principal 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
The identity equivalence between `` and CofiniteTopology .
Equations
- CofiniteTopology.of = Equiv.refl 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)}
:
@[simp]
theorem
continuous_prod_mk
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y}
{g : X → Z}
:
(Continuous fun (x : X) => (f x, g x)) ↔ Continuous f ∧ Continuous g
theorem
continuous_fst
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
Continuous Prod.fst
theorem
Continuous.fst
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y × Z}
(hf : Continuous f)
:
Continuous fun (x : X) => (f x).1
Postcomposing f with Prod.fst is continuous
theorem
Continuous.fst'
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Z}
(hf : Continuous f)
:
Continuous fun (x : X × Y) => f x.1
Precomposing f with Prod.fst is continuous
theorem
continuousAt_fst
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{p : X × Y}
:
ContinuousAt Prod.fst p
theorem
ContinuousAt.fst
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y × Z}
{x : X}
(hf : ContinuousAt f x)
:
ContinuousAt (fun (x : X) => (f x).1) x
Postcomposing f with Prod.fst is continuous at x
theorem
ContinuousAt.fst'
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Z}
{x : X}
{y : Y}
(hf : ContinuousAt f x)
:
ContinuousAt (fun (x : X × Y) => f x.1) (x, y)
Precomposing f with Prod.fst is continuous at (x, y)
theorem
ContinuousAt.fst''
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Z}
{x : X × Y}
(hf : ContinuousAt f x.1)
:
ContinuousAt (fun (x : X × Y) => f x.1) x
Precomposing f with Prod.fst is continuous at x : X × Y
theorem
Filter.Tendsto.fst_nhds
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace Y]
[TopologicalSpace Z]
{X : Type u_5}
{l : Filter X}
{f : X → Y × Z}
{p : Y × Z}
(h : Filter.Tendsto f l (nhds p))
:
Filter.Tendsto (fun (a : X) => (f a).1) l (nhds p.1)
theorem
continuous_snd
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
Continuous Prod.snd
theorem
Continuous.snd
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y × Z}
(hf : Continuous f)
:
Continuous fun (x : X) => (f x).2
Postcomposing f with Prod.snd is continuous
theorem
Continuous.snd'
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : Y → Z}
(hf : Continuous f)
:
Continuous fun (x : X × Y) => f x.2
Precomposing f with Prod.snd is continuous
theorem
continuousAt_snd
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{p : X × Y}
:
ContinuousAt Prod.snd p
theorem
ContinuousAt.snd
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y × Z}
{x : X}
(hf : ContinuousAt f x)
:
ContinuousAt (fun (x : X) => (f x).2) x
Postcomposing f with Prod.snd is continuous at x
theorem
ContinuousAt.snd'
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : Y → Z}
{x : X}
{y : Y}
(hf : ContinuousAt f y)
:
ContinuousAt (fun (x : X × Y) => f x.2) (x, y)
Precomposing f with Prod.snd is continuous at (x, y)
theorem
ContinuousAt.snd''
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : Y → Z}
{x : X × Y}
(hf : ContinuousAt f x.2)
:
ContinuousAt (fun (x : X × Y) => f x.2) x
Precomposing f with Prod.snd is continuous at x : X × Y
theorem
Filter.Tendsto.snd_nhds
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace Y]
[TopologicalSpace Z]
{X : Type u_5}
{l : Filter X}
{f : X → Y × Z}
{p : Y × Z}
(h : Filter.Tendsto f l (nhds p))
:
Filter.Tendsto (fun (a : X) => (f a).2) l (nhds p.2)
theorem
Continuous.prod_mk
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : Z → X}
{g : Z → Y}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun (x : Z) => (f x, g x)
theorem
Continuous.Prod.mk
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(x : X)
:
Continuous fun (y : Y) => (x, y)
theorem
Continuous.Prod.mk_left
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(y : Y)
:
Continuous fun (x : X) => (x, y)
theorem
IsClosed.setOf_mapsTo
{X : Type u}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Z]
{α : Type u_5}
{f : X → α → Z}
{s : Set α}
{t : Set Z}
(ht : IsClosed t)
(hf : ∀ a ∈ s, Continuous fun (x : X) => f x a)
:
IsClosed {x : X | Set.MapsTo (f x) s t}
If f x y is continuous in x for all y ∈ s,
then the set of x such that f x maps s to t is closed.
theorem
Continuous.comp₂
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{g : X × Y → Z}
(hg : Continuous g)
{e : W → X}
(he : Continuous e)
{f : W → Y}
(hf : Continuous f)
:
Continuous fun (w : W) => g (e w, f w)
theorem
Continuous.comp₃
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
{ε : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
[TopologicalSpace ε]
{g : X × Y × Z → ε}
(hg : Continuous g)
{e : W → X}
(he : Continuous e)
{f : W → Y}
(hf : Continuous f)
{k : W → Z}
(hk : Continuous k)
:
Continuous fun (w : W) => g (e w, f w, k w)
theorem
Continuous.comp₄
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
{ε : Type u_3}
{ζ : Type u_4}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
[TopologicalSpace ε]
[TopologicalSpace ζ]
{g : X × Y × Z × ζ → ε}
(hg : Continuous g)
{e : W → X}
(he : Continuous e)
{f : W → Y}
(hf : Continuous f)
{k : W → Z}
(hk : Continuous k)
{l : W → ζ}
(hl : Continuous l)
:
Continuous fun (w : W) => g (e w, f w, k w, l w)
theorem
Continuous.prodMap
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : Z → X}
{g : W → Y}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous (Prod.map f g)
@[deprecated Continuous.prodMap]
theorem
Continuous.prod_map
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : Z → X}
{g : W → Y}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous (Prod.map f g)
Alias of Continuous.prodMap.
theorem
continuous_inf_dom_left₂
{X : Type u_5}
{Y : Type u_6}
{Z : Type u_7}
{f : X → Y → Z}
{ta1 : TopologicalSpace X}
{ta2 : TopologicalSpace X}
{tb1 : TopologicalSpace Y}
{tb2 : TopologicalSpace Y}
{tc1 : TopologicalSpace Z}
(h : Continuous fun (p : X × Y) => f p.1 p.2)
:
Continuous fun (p : X × Y) => f p.1 p.2
A version of continuous_inf_dom_left for binary functions
theorem
continuous_inf_dom_right₂
{X : Type u_5}
{Y : Type u_6}
{Z : Type u_7}
{f : X → Y → Z}
{ta1 : TopologicalSpace X}
{ta2 : TopologicalSpace X}
{tb1 : TopologicalSpace Y}
{tb2 : TopologicalSpace Y}
{tc1 : TopologicalSpace Z}
(h : Continuous fun (p : X × Y) => f p.1 p.2)
:
Continuous fun (p : X × Y) => f p.1 p.2
A version of continuous_inf_dom_right for binary functions
theorem
continuous_sInf_dom₂
{X : Type u_5}
{Y : Type u_6}
{Z : Type u_7}
{f : X → Y → Z}
{tas : Set (TopologicalSpace X)}
{tbs : Set (TopologicalSpace Y)}
{tX : TopologicalSpace X}
{tY : TopologicalSpace Y}
{tc : TopologicalSpace Z}
(hX : tX ∈ tas)
(hY : tY ∈ tbs)
(hf : Continuous fun (p : X × Y) => f p.1 p.2)
:
Continuous fun (p : X × Y) => f p.1 p.2
A version of continuous_sInf_dom for binary functions
theorem
Filter.Eventually.prod_inl_nhds
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{p : X → Prop}
{x : X}
(h : ∀ᶠ (x : X) in nhds x, p x)
(y : Y)
:
theorem
Filter.Eventually.prod_inr_nhds
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{p : Y → Prop}
{y : Y}
(h : ∀ᶠ (x : Y) in nhds y, p x)
(x : X)
:
theorem
Filter.Eventually.prod_mk_nhds
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{px : X → Prop}
{x : X}
(hx : ∀ᶠ (x : X) in nhds x, px x)
{py : Y → Prop}
{y : Y}
(hy : ∀ᶠ (y : Y) in nhds y, py y)
:
theorem
continuous_swap
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
Continuous Prod.swap
theorem
isClosedMap_swap
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsClosedMap Prod.swap
theorem
Continuous.uncurry_left
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y → Z}
(x : X)
(h : Continuous (Function.uncurry f))
:
Continuous (f x)
theorem
Continuous.uncurry_right
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y → Z}
(y : Y)
(h : Continuous (Function.uncurry f))
:
Continuous fun (a : X) => f a y
@[deprecated Continuous.uncurry_left]
theorem
continuous_uncurry_left
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y → Z}
(x : X)
(h : Continuous (Function.uncurry f))
:
Continuous (f x)
Alias of Continuous.uncurry_left.
@[deprecated Continuous.uncurry_right]
theorem
continuous_uncurry_right
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y → Z}
(y : Y)
(h : Continuous (Function.uncurry f))
:
Continuous fun (a : X) => f a y
Alias of Continuous.uncurry_right.
theorem
continuous_curry
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{g : X × Y → Z}
(x : X)
(h : Continuous g)
:
Continuous (Function.curry g x)
theorem
IsOpen.prod
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Set X}
{t : Set Y}
(hs : IsOpen s)
(ht : IsOpen t)
:
theorem
nhds_prod_eq
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{x : X}
{y : Y}
:
theorem
nhdsWithin_prod_eq
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(x : X)
(y : Y)
(s : Set X)
(t : Set Y)
:
nhdsWithin (x, y) (s ×ˢ t) = nhdsWithin x s ×ˢ nhdsWithin y t
instance
Prod.instNeBotNhdsWithinIio
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
[Preorder X]
[Preorder Y]
{x : X × Y}
[hx₁ : (nhdsWithin x.1 (Set.Iio x.1)).NeBot]
[hx₂ : (nhdsWithin x.2 (Set.Iio x.2)).NeBot]
:
(nhdsWithin x (Set.Iio x)).NeBot
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
theorem
mem_nhds_prod_iff
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{x : X}
{y : Y}
{s : Set (X × Y)}
:
theorem
mem_nhdsWithin_prod_iff
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{x : X}
{y : Y}
{s : Set (X × Y)}
{tx : Set X}
{ty : Set Y}
:
s ∈ nhdsWithin (x, y) (tx ×ˢ ty) ↔ ∃ u ∈ nhdsWithin x tx, ∃ v ∈ nhdsWithin y ty, u ×ˢ v ⊆ s
theorem
Filter.HasBasis.prod_nhds
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{ιX : Type u_5}
{ιY : Type u_6}
{px : ιX → Prop}
{py : ιY → Prop}
{sx : ιX → Set X}
{sy : ιY → Set Y}
{x : X}
{y : Y}
(hx : (nhds x).HasBasis px sx)
(hy : (nhds y).HasBasis py sy)
:
theorem
Filter.HasBasis.prod_nhds'
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{ιX : Type u_5}
{ιY : Type u_6}
{pX : ιX → Prop}
{pY : ιY → Prop}
{sx : ιX → Set X}
{sy : ιY → Set Y}
{p : X × Y}
(hx : (nhds p.1).HasBasis pX sx)
(hy : (nhds p.2).HasBasis pY sy)
:
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
Prod.tendsto_iff
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace Y]
[TopologicalSpace Z]
{X : Type u_5}
(seq : X → Y × Z)
{f : Filter X}
(p : Y × Z)
:
Filter.Tendsto seq f (nhds p) ↔ Filter.Tendsto (fun (n : X) => (seq n).1) f (nhds p.1) ∧ Filter.Tendsto (fun (n : X) => (seq n).2) f (nhds p.2)
instance
instDiscreteTopologyProd
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
[DiscreteTopology X]
[DiscreteTopology Y]
:
DiscreteTopology (X × Y)
Equations
- ⋯ = ⋯
theorem
prod_mem_nhds
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Set X}
{t : Set Y}
{x : X}
{y : Y}
(hx : s ∈ nhds x)
(hy : t ∈ nhds y)
:
theorem
Filter.Eventually.prod_nhds
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{p : X → Prop}
{q : Y → Prop}
{x : X}
{y : Y}
(hx : ∀ᶠ (x : X) in nhds x, p x)
(hy : ∀ᶠ (y : Y) in nhds y, q y)
:
theorem
nhds_swap
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(x : X)
(y : Y)
:
nhds (x, y) = Filter.map Prod.swap (nhds (y, x))
theorem
Filter.Tendsto.prod_mk_nhds
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{γ : Type u_5}
{x : X}
{y : Y}
{f : Filter γ}
{mx : γ → X}
{my : γ → Y}
(hx : Filter.Tendsto mx f (nhds x))
(hy : Filter.Tendsto my f (nhds y))
:
Filter.Tendsto (fun (c : γ) => (mx c, my c)) f (nhds (x, y))
theorem
Filter.Eventually.curry_nhds
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{p : X × Y → Prop}
{x : X}
{y : Y}
(h : ∀ᶠ (x : X × Y) in nhds (x, y), p x)
:
theorem
ContinuousAt.prod
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y}
{g : X → Z}
{x : X}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (fun (x : X) => (f x, g x)) x
theorem
ContinuousAt.prodMap
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Z}
{g : Y → W}
{p : X × Y}
(hf : ContinuousAt f p.1)
(hg : ContinuousAt g p.2)
:
ContinuousAt (Prod.map f g) p
@[deprecated ContinuousAt.prodMap]
theorem
ContinuousAt.prod_map
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Z}
{g : Y → W}
{p : X × Y}
(hf : ContinuousAt f p.1)
(hg : ContinuousAt g p.2)
:
ContinuousAt (Prod.map f g) p
Alias of ContinuousAt.prodMap.
theorem
ContinuousAt.prodMap'
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Z}
{g : Y → W}
{x : X}
{y : Y}
(hf : ContinuousAt f x)
(hg : ContinuousAt g y)
:
ContinuousAt (Prod.map f g) (x, y)
A version of ContinuousAt.prodMap that avoids Prod.fst/Prod.snd
by assuming that the point is (x, y).
@[deprecated ContinuousAt.prodMap']
theorem
ContinuousAt.prod_map'
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Z}
{g : Y → W}
{x : X}
{y : Y}
(hf : ContinuousAt f x)
(hg : ContinuousAt g y)
:
ContinuousAt (Prod.map f g) (x, y)
Alias of ContinuousAt.prodMap'.
A version of ContinuousAt.prodMap that avoids Prod.fst/Prod.snd
by assuming that the point is (x, y).
theorem
ContinuousAt.comp₂
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : Y × Z → W}
{g : X → Y}
{h : X → Z}
{x : X}
(hf : ContinuousAt f (g x, h x))
(hg : ContinuousAt g x)
(hh : ContinuousAt h x)
:
ContinuousAt (fun (x : X) => f (g x, h x)) x
theorem
ContinuousAt.comp₂_of_eq
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : Y × Z → W}
{g : X → Y}
{h : X → Z}
{x : X}
{y : Y × Z}
(hf : ContinuousAt f y)
(hg : ContinuousAt g x)
(hh : ContinuousAt h x)
(e : (g x, h x) = y)
:
ContinuousAt (fun (x : X) => f (g x, h x)) x
theorem
Continuous.curry_left
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X × Y → Z}
(hf : Continuous f)
{y : Y}
:
Continuous fun (x : X) => f (x, y)
Continuous functions on products are continuous in their first argument
theorem
Continuous.along_fst
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X × Y → Z}
(hf : Continuous f)
{y : Y}
:
Continuous fun (x : X) => f (x, y)
Alias of Continuous.curry_left.
Continuous functions on products are continuous in their first argument
theorem
Continuous.curry_right
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X × Y → Z}
(hf : Continuous f)
{x : X}
:
Continuous fun (y : Y) => f (x, y)
Continuous functions on products are continuous in their second argument
theorem
Continuous.along_snd
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X × Y → Z}
(hf : Continuous f)
{x : X}
:
Continuous fun (y : Y) => f (x, y)
Alias of Continuous.curry_right.
Continuous functions on products are continuous in their second argument
theorem
prod_induced_induced
{Y : Type v}
{W : Type u_2}
[TopologicalSpace Y]
[TopologicalSpace W]
{X : Type u_5}
{Z : Type u_6}
(f : X → Y)
(g : Z → W)
:
instTopologicalSpaceProd = TopologicalSpace.induced (fun (p : X × Z) => (f p.1, g p.2)) instTopologicalSpaceProd
A product of induced topologies is induced by the product map
theorem
map_fst_nhdsWithin
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(x : X × Y)
:
Filter.map Prod.fst (nhdsWithin x (Prod.snd ⁻¹' {x.2})) = nhds x.1
Prod.fst maps neighborhood of x : X × Y within the section Prod.snd ⁻¹' {x.2}
to 𝓝 x.1.
@[simp]
theorem
map_fst_nhds
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(x : X × Y)
:
Filter.map Prod.fst (nhds x) = nhds x.1
theorem
isOpenMap_fst
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsOpenMap Prod.fst
The first projection in a product of topological spaces sends open sets to open sets.
theorem
map_snd_nhdsWithin
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(x : X × Y)
:
Filter.map Prod.snd (nhdsWithin x (Prod.fst ⁻¹' {x.1})) = nhds x.2
Prod.snd maps neighborhood of x : X × Y within the section Prod.fst ⁻¹' {x.1}
to 𝓝 x.2.
@[simp]
theorem
map_snd_nhds
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(x : X × Y)
:
Filter.map Prod.snd (nhds x) = nhds x.2
theorem
isOpenMap_snd
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsOpenMap Prod.snd
The second projection in a product of topological spaces sends open sets to open sets.
theorem
isQuotientMap_fst
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
[Nonempty Y]
:
IsQuotientMap Prod.fst
@[deprecated isQuotientMap_fst]
theorem
quotientMap_fst
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
[Nonempty Y]
:
IsQuotientMap Prod.fst
Alias of isQuotientMap_fst.
theorem
isQuotientMap_snd
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
[Nonempty X]
:
IsQuotientMap Prod.snd
@[deprecated isQuotientMap_snd]
theorem
quotientMap_snd
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
[Nonempty X]
:
IsQuotientMap Prod.snd
Alias of isQuotientMap_snd.
theorem
closure_prod_eq
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Set X}
{t : Set Y}
:
theorem
interior_prod_eq
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(s : Set X)
(t : Set Y)
:
@[simp]
theorem
frontier_prod_univ_eq
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(s : Set X)
:
@[simp]
theorem
frontier_univ_prod_eq
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(s : Set Y)
:
theorem
map_mem_closure₂
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y → Z}
{x : X}
{y : Y}
{s : Set X}
{t : Set Y}
{u : Set Z}
(hf : Continuous (Function.uncurry f))
(hx : x ∈ closure s)
(hy : y ∈ closure t)
(h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u)
:
theorem
IsClosed.prod
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{s₁ : Set X}
{s₂ : Set Y}
(h₁ : IsClosed s₁)
(h₂ : IsClosed s₂)
:
theorem
Dense.prod
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Set X}
{t : Set Y}
(hs : Dense s)
(ht : Dense t)
:
The product of two dense sets is a dense set.
theorem
DenseRange.prodMap
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace Y]
[TopologicalSpace Z]
{ι : Type u_5}
{κ : Type u_6}
{f : ι → Y}
{g : κ → Z}
(hf : DenseRange f)
(hg : DenseRange g)
:
DenseRange (Prod.map f g)
If f and g are maps with dense range, then Prod.map f g has dense range.
@[deprecated DenseRange.prodMap]
theorem
DenseRange.prod_map
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace Y]
[TopologicalSpace Z]
{ι : Type u_5}
{κ : Type u_6}
{f : ι → Y}
{g : κ → Z}
(hf : DenseRange f)
(hg : DenseRange g)
:
DenseRange (Prod.map f g)
Alias of DenseRange.prodMap.
If f and g are maps with dense range, then Prod.map f g has dense range.
theorem
IsInducing.prodMap
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Y}
{g : Z → W}
(hf : IsInducing f)
(hg : IsInducing g)
:
IsInducing (Prod.map f g)
@[deprecated IsInducing.prodMap]
theorem
Inducing.prodMap
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Y}
{g : Z → W}
(hf : IsInducing f)
(hg : IsInducing g)
:
IsInducing (Prod.map f g)
Alias of IsInducing.prodMap.
@[deprecated IsInducing.prodMap]
theorem
Inducing.prod_map
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Y}
{g : Z → W}
(hf : IsInducing f)
(hg : IsInducing g)
:
IsInducing (Prod.map f g)
Alias of IsInducing.prodMap.
@[simp]
theorem
isInducing_const_prod
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{x : X}
{f : Y → Z}
:
(IsInducing fun (x' : Y) => (x, f x')) ↔ IsInducing f
@[deprecated isInducing_const_prod]
theorem
inducing_const_prod
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{x : X}
{f : Y → Z}
:
(IsInducing fun (x' : Y) => (x, f x')) ↔ IsInducing f
Alias of isInducing_const_prod.
@[simp]
theorem
isInducing_prod_const
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{y : Y}
{f : X → Z}
:
(IsInducing fun (x : X) => (f x, y)) ↔ IsInducing f
@[deprecated isInducing_prod_const]
theorem
inducing_prod_const
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{y : Y}
{f : X → Z}
:
(IsInducing fun (x : X) => (f x, y)) ↔ IsInducing f
Alias of isInducing_prod_const.
theorem
IsEmbedding.prodMap
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Y}
{g : Z → W}
(hf : IsEmbedding f)
(hg : IsEmbedding g)
:
IsEmbedding (Prod.map f g)
@[deprecated IsEmbedding.prodMap]
theorem
Embedding.prodMap
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Y}
{g : Z → W}
(hf : IsEmbedding f)
(hg : IsEmbedding g)
:
IsEmbedding (Prod.map f g)
Alias of IsEmbedding.prodMap.
@[deprecated Embedding.prodMap]
theorem
Embedding.prod_map
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Y}
{g : Z → W}
(hf : IsEmbedding f)
(hg : IsEmbedding g)
:
IsEmbedding (Prod.map f g)
Alias of IsEmbedding.prodMap.
Alias of IsEmbedding.prodMap.
theorem
IsOpenMap.prodMap
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Y}
{g : Z → W}
(hf : IsOpenMap f)
(hg : IsOpenMap g)
:
@[deprecated IsOpenMap.prodMap]
theorem
IsOpenMap.prod
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Y}
{g : Z → W}
(hf : IsOpenMap f)
(hg : IsOpenMap g)
:
Alias of IsOpenMap.prodMap.
theorem
IsOpenEmbedding.prodMap
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Y}
{g : Z → W}
(hf : IsOpenEmbedding f)
(hg : IsOpenEmbedding g)
:
IsOpenEmbedding (Prod.map f g)
@[deprecated IsOpenEmbedding.prodMap]
theorem
OpenEmbedding.prodMap
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Y}
{g : Z → W}
(hf : IsOpenEmbedding f)
(hg : IsOpenEmbedding g)
:
IsOpenEmbedding (Prod.map f g)
Alias of IsOpenEmbedding.prodMap.
@[deprecated IsOpenEmbedding.prodMap]
theorem
IsOpenEmbedding.prod
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Y}
{g : Z → W}
(hf : IsOpenEmbedding f)
(hg : IsOpenEmbedding g)
:
IsOpenEmbedding (Prod.map f g)
Alias of IsOpenEmbedding.prodMap.
theorem
isEmbedding_graph
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : Continuous f)
:
IsEmbedding fun (x : X) => (x, f x)
@[deprecated isEmbedding_graph]
theorem
embedding_graph
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : Continuous f)
:
IsEmbedding fun (x : X) => (x, f x)
Alias of isEmbedding_graph.
theorem
isEmbedding_prodMk
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(x : X)
:
IsEmbedding (Prod.mk x)
@[deprecated isEmbedding_prodMk]
theorem
embedding_prod_mk
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(x : X)
:
IsEmbedding (Prod.mk x)
Alias of isEmbedding_prodMk.
theorem
IsOpenQuotientMap.prodMap
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Y}
{g : Z → W}
(hf : IsOpenQuotientMap f)
(hg : IsOpenQuotientMap g)
:
IsOpenQuotientMap (Prod.map f g)
theorem
continuous_bool_rng
{X : Type u}
[TopologicalSpace X]
{f : X → Bool}
(b : Bool)
:
Continuous f ↔ IsClopen (f ⁻¹' {b})
theorem
continuous_sum_dom
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X ⊕ Y → Z}
:
Continuous f ↔ Continuous (f ∘ Sum.inl) ∧ Continuous (f ∘ Sum.inr)
theorem
continuous_sum_elim
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Z}
{g : Y → Z}
:
Continuous (Sum.elim f g) ↔ Continuous f ∧ Continuous g
theorem
Continuous.sum_elim
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Z}
{g : Y → Z}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous (Sum.elim f g)
theorem
continuous_isLeft
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
Continuous Sum.isLeft
theorem
continuous_isRight
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
Continuous Sum.isRight
theorem
continuous_inl
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
Continuous Sum.inl
theorem
continuous_inr
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
Continuous Sum.inr
theorem
continuous_sum_swap
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
Continuous Sum.swap
theorem
isOpen_sum_iff
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Set (X ⊕ Y)}
:
theorem
isClosed_sum_iff
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Set (X ⊕ Y)}
:
theorem
isOpenMap_inl
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsOpenMap Sum.inl
theorem
isOpenMap_inr
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsOpenMap Sum.inr
theorem
isOpenEmbedding_inl
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsOpenEmbedding Sum.inl
@[deprecated isOpenEmbedding_inl]
theorem
openEmbedding_inl
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsOpenEmbedding Sum.inl
Alias of isOpenEmbedding_inl.
theorem
isOpenEmbedding_inr
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsOpenEmbedding Sum.inr
@[deprecated isOpenEmbedding_inr]
theorem
openEmbedding_inr
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsOpenEmbedding Sum.inr
Alias of isOpenEmbedding_inr.
theorem
IsEmbedding.inl
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsEmbedding Sum.inl
theorem
IsEmbedding.inr
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsEmbedding Sum.inr
@[deprecated IsEmbedding.inr]
theorem
embedding_inr
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsEmbedding Sum.inr
Alias of IsEmbedding.inr.
theorem
isClosedEmbedding_inl
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsClosedEmbedding Sum.inl
@[deprecated isClosedEmbedding_inl]
theorem
closedEmbedding_inl
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsClosedEmbedding Sum.inl
Alias of isClosedEmbedding_inl.
theorem
isClosedEmbedding_inr
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsClosedEmbedding Sum.inr
@[deprecated isClosedEmbedding_inr]
theorem
closedEmbedding_inr
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
:
IsClosedEmbedding Sum.inr
Alias of isClosedEmbedding_inr.
theorem
nhds_inl
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(x : X)
:
nhds (Sum.inl x) = Filter.map Sum.inl (nhds x)
theorem
nhds_inr
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
(y : Y)
:
nhds (Sum.inr y) = Filter.map Sum.inr (nhds y)
@[simp]
theorem
continuous_sum_map
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Y}
{g : Z → W}
:
Continuous (Sum.map f g) ↔ Continuous f ∧ Continuous g
theorem
Continuous.sum_map
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Y}
{g : Z → W}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous (Sum.map f g)
theorem
isOpenMap_sum
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X ⊕ Y → Z}
:
theorem
IsOpenMap.sumMap
{X : Type u}
{Y : Type v}
{Z : Type u_1}
{W : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[TopologicalSpace W]
{f : X → Y}
{g : Z → W}
(hf : IsOpenMap f)
(hg : IsOpenMap g)
:
@[simp]
theorem
isOpenMap_sum_elim
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Z}
{g : Y → Z}
:
theorem
IsOpenMap.sum_elim
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Z}
{g : Y → Z}
(hf : IsOpenMap f)
(hg : IsOpenMap g)
:
theorem
isClosedMap_sum
{X : Type u}
{Y : Type v}
{Z : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X ⊕ Y → Z}
:
IsClosedMap f ↔ (IsClosedMap fun (a : X) => f (Sum.inl a)) ∧ IsClosedMap fun (b : Y) => f (Sum.inr b)
@[deprecated IsInducing.subtypeVal]
Alias of IsInducing.subtypeVal.
theorem
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 IsInducing.of_codRestrict]
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 : IsInducing (Set.codRestrict f t ht))
:
Alias of IsInducing.of_codRestrict.
theorem
IsEmbedding.subtypeVal
{X : Type u}
[TopologicalSpace X]
{p : X → Prop}
:
IsEmbedding Subtype.val
@[deprecated IsEmbedding.subtypeVal]
theorem
embedding_subtype_val
{X : Type u}
[TopologicalSpace X]
{p : X → Prop}
:
IsEmbedding Subtype.val
Alias of IsEmbedding.subtypeVal.
theorem
IsClosedEmbedding.subtypeVal
{X : Type u}
[TopologicalSpace X]
{p : X → Prop}
(h : IsClosed {a : X | p a})
:
IsClosedEmbedding Subtype.val
@[deprecated IsClosedEmbedding.subtypeVal]
theorem
closedEmbedding_subtype_val
{X : Type u}
[TopologicalSpace X]
{p : X → Prop}
(h : IsClosed {a : X | p a})
:
IsClosedEmbedding Subtype.val
Alias of IsClosedEmbedding.subtypeVal.
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)
:
IsOpenEmbedding Subtype.val
@[deprecated IsOpen.isOpenEmbedding_subtypeVal]
theorem
IsOpen.openEmbedding_subtype_val
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(hs : IsOpen s)
:
IsOpenEmbedding Subtype.val
Alias of IsOpen.isOpenEmbedding_subtypeVal.
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)
:
IsOpenMap (s.restrict f)
theorem
IsClosed.isClosedEmbedding_subtypeVal
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(hs : IsClosed s)
:
IsClosedEmbedding Subtype.val
@[deprecated IsClosed.isClosedEmbedding_subtypeVal]
theorem
IsClosed.closedEmbedding_subtype_val
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(hs : IsClosed s)
:
IsClosedEmbedding Subtype.val
Alias of IsClosed.isClosedEmbedding_subtypeVal.
theorem
IsClosed.isClosedMap_subtype_val
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(hs : IsClosed s)
:
IsClosedMap Subtype.val
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
continuous_inclusion
{X : Type u}
[TopologicalSpace X]
{s : Set X}
{t : Set X}
(h : s ⊆ t)
:
theorem
continuousAt_subtype_val
{X : Type u}
[TopologicalSpace X]
{p : X → Prop}
{x : Subtype p}
:
ContinuousAt Subtype.val x
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)
@[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
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
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 IsInducing.codRestrict]
theorem
Inducing.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)
Alias of IsInducing.codRestrict.
theorem
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 IsEmbedding.codRestrict]
theorem
Embedding.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)
Alias of IsEmbedding.codRestrict.
theorem
IsEmbedding.inclusion
{X : Type u}
[TopologicalSpace X]
{s : Set X}
{t : Set X}
(h : s ⊆ t)
:
@[deprecated IsEmbedding.inclusion]
Alias of IsEmbedding.inclusion.
theorem
DiscreteTopology.of_subset
{X : Type u_5}
[TopologicalSpace X]
{s : Set X}
{t : Set X}
:
DiscreteTopology ↑s → 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
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)
:
IsQuotientMap (s.restrictPreimage f)
If f : X → Y is a quotient map,
then its restriction to the preimage of an open set is a quotient map too.
@[deprecated IsQuotientMap.restrictPreimage_isOpen]
theorem
QuotientMap.restrictPreimage_isOpen
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : IsQuotientMap f)
{s : Set Y}
(hs : IsOpen s)
:
IsQuotientMap (s.restrictPreimage f)
Alias of 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
isQuotientMap_quot_mk
{X : Type u}
[TopologicalSpace X]
{r : X → X → Prop}
:
IsQuotientMap (Quot.mk r)
@[deprecated isQuotientMap_quot_mk]
theorem
quotientMap_quot_mk
{X : Type u}
[TopologicalSpace X]
{r : X → X → Prop}
:
IsQuotientMap (Quot.mk r)
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)
theorem
isQuotientMap_quotient_mk'
{X : Type u}
[TopologicalSpace X]
{s : Setoid X}
:
IsQuotientMap Quotient.mk'
@[deprecated isQuotientMap_quotient_mk']
theorem
quotientMap_quotient_mk'
{X : Type u}
[TopologicalSpace X]
{s : Setoid X}
:
IsQuotientMap Quotient.mk'
Alias of 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 : (⇑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}
:
Continuous f ↔ ∀ (i : ι), Continuous fun (a : X) => f a 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
Filter.Tendsto.apply_nhds
{Y : Type v}
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{l : Filter Y}
{f : Y → (i : ι) → π i}
{x : (i : ι) → π i}
(h : Filter.Tendsto f l (nhds x))
(i : ι)
:
Filter.Tendsto (fun (a : Y) => f a i) l (nhds (x 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}
:
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}
{π : ι → Type u_6}
[TopologicalSpace X]
[T : (i : ι) → TopologicalSpace (π i)]
{f : X → (i : ι) → π i}
{x : X}
:
ContinuousAt f x ↔ ∀ (i : ι), ContinuousAt (fun (y : X) => f y i) 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
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)) Pi.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 ∘ φ) Pi.topologicalSpace = ⨅ (i' : ι'), TopologicalSpace.induced (Function.eval (φ i')) inst✝
theorem
Pi.continuous_restrict
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
(S : Set ι)
:
Continuous S.restrict
theorem
Pi.continuous_restrict₂
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{s : Set ι}
{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 ι)
:
Continuous s.restrict
theorem
Finset.continuous_restrict₂
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{s : Finset ι}
{t : Finset ι}
(hst : s ⊆ t)
:
Continuous (Finset.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 : Set X}
{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 : Finset X}
{t : Finset X}
(hst : s ⊆ t)
{f : { x : X // x ∈ t } → Z}
(hf : Continuous f)
:
Continuous (Finset.restrict₂ hst f)
theorem
Pi.induced_restrict
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
(S : Set ι)
:
TopologicalSpace.induced S.restrict Pi.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 ι))
:
TopologicalSpace.induced (⋃₀ 𝔖).restrict Pi.topologicalSpace = ⨅ S ∈ 𝔖, TopologicalSpace.induced S.restrict Pi.topologicalSpace
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 : Filter.Tendsto f l (nhds x))
(i : ι)
{g : Y → π i}
{xi : π i}
(hg : Filter.Tendsto g l (nhds xi))
:
Filter.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_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
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
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}
{l : Filter Y}
{x : π i}
(hf : Filter.Tendsto f l (nhds x))
{g : Y → (j : Fin n) → π (i.succAbove j)}
{y : (j : Fin n) → π (i.succAbove j)}
(hg : Filter.Tendsto g l (nhds y))
:
Filter.Tendsto (fun (a : Y) => i.insertNth (f a) (g a)) l (nhds (i.insertNth x y))
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}
{x : X}
(hf : ContinuousAt f x)
{g : X → (j : Fin n) → π (i.succAbove j)}
(hg : ContinuousAt g x)
:
ContinuousAt (fun (a : X) => i.insertNth (f a) (g a)) x
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}
(hf : Continuous f)
{g : X → (j : Fin n) → π (i.succAbove j)}
(hg : Continuous g)
:
Continuous fun (a : X) => i.insertNth (f a) (g a)
theorem
isOpen_set_pi
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{i : Set ι}
{s : (a : ι) → Set (π a)}
(hi : i.Finite)
(hs : ∀ a ∈ i, IsOpen (s a))
:
IsOpen (i.pi s)
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))
:
IsClosed (i.pi s)
theorem
interior_pi_set
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{I : Set ι}
(hI : I.Finite)
{s : (i : ι) → Set (π i)}
:
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)
:
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.
Equations
- ⋯ = ⋯
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
isOpenEmbedding_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
@[deprecated isOpenEmbedding_sigmaMk]
theorem
openEmbedding_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
Alias of isOpenEmbedding_sigmaMk.
theorem
isClosedEmbedding_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
@[deprecated isClosedEmbedding_sigmaMk]
theorem
closedEmbedding_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
Alias of isClosedEmbedding_sigmaMk.
theorem
IsEmbedding.sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
IsEmbedding (Sigma.mk i)
@[deprecated IsEmbedding.sigmaMk]
theorem
embedding_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
IsEmbedding (Sigma.mk i)
Alias of IsEmbedding.sigmaMk.
theorem
Sigma.nhds_mk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
(i : ι)
(x : σ i)
:
nhds ⟨i, x⟩ = Filter.map (Sigma.mk i) (nhds x)
theorem
Sigma.nhds_eq
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
(x : Sigma σ)
:
nhds x = Filter.map (Sigma.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}
:
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
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)
@[deprecated isInducing_sigmaMap]
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₁)
:
IsInducing (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsInducing (f₂ i)
Alias of isInducing_sigmaMap.
theorem
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)
@[deprecated isEmbedding_sigmaMap]
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₁)
:
IsEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsEmbedding (f₂ i)
Alias of isEmbedding_sigmaMap.
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₁)
:
IsOpenEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsOpenEmbedding (f₂ i)
@[deprecated isOpenEmbedding_sigma_map]
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₁)
:
IsOpenEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsOpenEmbedding (f₂ i)
Alias of isOpenEmbedding_sigma_map.
@[deprecated IsEmbedding.uliftDown]
Alias of IsEmbedding.uliftDown.
theorem
ULift.isClosedEmbedding_down
{X : Type u}
[TopologicalSpace X]
:
IsClosedEmbedding ULift.down
@[deprecated ULift.isClosedEmbedding_down]
Alias of ULift.isClosedEmbedding_down.
Equations
- ⋯ = ⋯
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)
: