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
Equations
- instTopologicalSpaceSubtype = TopologicalSpace.induced Subtype.val t
instance
instTopologicalSpaceQuot
{α : Type u}
{r : α → α → Prop}
[t : TopologicalSpace α]
:
TopologicalSpace (Quot r)
Equations
- instTopologicalSpaceQuot = TopologicalSpace.coinduced (Quot.mk r) t
Equations
- instTopologicalSpaceQuotient = TopologicalSpace.coinduced Quotient.mk' t
instance
instTopologicalSpaceProd
{α : Type u}
{β : Type v}
[t₁ : TopologicalSpace α]
[t₂ : TopologicalSpace β]
:
TopologicalSpace (α × β)
Equations
- instTopologicalSpaceProd = TopologicalSpace.induced Prod.fst t₁ ⊓ TopologicalSpace.induced Prod.snd t₂
instance
instTopologicalSpaceSum
{α : Type u}
{β : Type v}
[t₁ : TopologicalSpace α]
[t₂ : TopologicalSpace β]
:
TopologicalSpace (α ⊕ β)
Equations
- instTopologicalSpaceSum = TopologicalSpace.coinduced Sum.inl t₁ ⊔ TopologicalSpace.coinduced Sum.inr t₂
instance
instTopologicalSpaceSigma
{α : Type u}
{β : α → Type v}
[t₂ : (a : α) → TopologicalSpace (β a)]
:
Equations
- instTopologicalSpaceSigma = ⨆ (a : α), TopologicalSpace.coinduced (Sigma.mk a) (t₂ a)
instance
Pi.topologicalSpace
{α : Type u}
{β : α → Type v}
[t₂ : (a : α) → TopologicalSpace (β a)]
:
TopologicalSpace ((a : α) → β a)
Equations
- Pi.topologicalSpace = ⨅ (a : α), TopologicalSpace.induced (fun f => f a) (t₂ a)
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
instance
instDiscreteTopologyAdditiveInstTopologicalSpaceAdditive
{α : Type u}
[TopologicalSpace α]
[DiscreteTopology α]
:
Equations
- (_ : DiscreteTopology (Additive α)) = inst
instance
instDiscreteTopologyMultiplicativeInstTopologicalSpaceMultiplicative
{α : Type u}
[TopologicalSpace α]
[DiscreteTopology α]
:
Equations
- (_ : DiscreteTopology (Multiplicative α)) = inst
theorem
nhds_ofMul
{α : Type u}
[TopologicalSpace α]
(a : α)
:
nhds (↑Additive.ofMul a) = Filter.map (↑Additive.ofMul) (nhds a)
theorem
nhds_ofAdd
{α : Type u}
[TopologicalSpace α]
(a : α)
:
nhds (↑Multiplicative.ofAdd a) = Filter.map (↑Multiplicative.ofAdd) (nhds a)
theorem
nhds_toMul
{α : Type u}
[TopologicalSpace α]
(a : Additive α)
:
nhds (↑Additive.toMul a) = Filter.map (↑Additive.toMul) (nhds a)
theorem
nhds_toAdd
{α : Type u}
[TopologicalSpace α]
(a : Multiplicative α)
:
nhds (↑Multiplicative.toAdd a) = Filter.map (↑Multiplicative.toAdd) (nhds a)
Order dual #
The topology on this type synonym is inherited without change.
Equations
- instTopologicalSpaceOrderDual = inst
instance
instDiscreteTopologyOrderDualInstTopologicalSpaceOrderDual
{α : Type u}
[TopologicalSpace α]
[DiscreteTopology α]
:
Equations
- (_ : DiscreteTopology αᵒᵈ) = inst
theorem
nhds_toDual
{α : Type u}
[TopologicalSpace α]
(a : α)
:
nhds (↑OrderDual.toDual a) = Filter.map (↑OrderDual.toDual) (nhds a)
theorem
nhds_ofDual
{α : Type u}
[TopologicalSpace α]
(a : α)
:
nhds (↑OrderDual.ofDual a) = Filter.map (↑OrderDual.ofDual) (nhds a)
theorem
Quotient.preimage_mem_nhds
{α : Type u}
[TopologicalSpace α]
[s : Setoid α]
{V : Set (Quotient s)}
{a : α}
(hs : V ∈ nhds (Quotient.mk' a))
:
The image of a dense set under Quotient.mk' is a dense set.
theorem
DenseRange.quotient
{α : Type u}
{β : Type v}
[Setoid α]
[TopologicalSpace α]
{f : β → α}
(hf : DenseRange f)
:
DenseRange (Quotient.mk' ∘ f)
The composition of Quotient.mk' and a function with dense range has dense range.
instance
Sum.discreteTopology
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
[hα : DiscreteTopology α]
[hβ : DiscreteTopology β]
:
DiscreteTopology (α ⊕ β)
instance
Sigma.discreteTopology
{α : Type u}
{β : α → Type v}
[(a : α) → TopologicalSpace (β a)]
[h : ∀ (a : α), DiscreteTopology (β a)]
:
theorem
nhds_subtype
{α : Type u}
[TopologicalSpace α]
(s : Set α)
(a : { x // x ∈ s })
:
nhds a = Filter.comap Subtype.val (nhds ↑a)
theorem
nhdsWithin_subtype_eq_bot_iff
{α : Type u}
[TopologicalSpace α]
{s : Set α}
{t : Set α}
{x : ↑s}
:
nhdsWithin x (Subtype.val ⁻¹' t) = ⊥ ↔ nhdsWithin (↑x) t ⊓ Filter.principal s = ⊥
theorem
nhds_ne_subtype_eq_bot_iff
{α : Type u}
[TopologicalSpace α]
{S : Set α}
{x : ↑S}
:
nhdsWithin x {x}ᶜ = ⊥ ↔ nhdsWithin ↑x {↑x}ᶜ ⊓ Filter.principal S = ⊥
theorem
nhds_ne_subtype_neBot_iff
{α : Type u}
[TopologicalSpace α]
{S : Set α}
{x : ↑S}
:
Filter.NeBot (nhdsWithin x {x}ᶜ) ↔ Filter.NeBot (nhdsWithin ↑x {↑x}ᶜ ⊓ Filter.principal S)
theorem
discreteTopology_subtype_iff
{α : Type u}
[TopologicalSpace α]
{S : Set α}
:
DiscreteTopology ↑S ↔ ∀ (x : α), 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 α = α
Instances For
The identity equivalence between α and CofiniteTopology α.
Equations
- CofiniteTopology.of = Equiv.refl α
Instances For
Equations
- CofiniteTopology.instInhabitedCofiniteTopology = { default := ↑CofiniteTopology.of default }
Equations
- One or more equations did not get rendered due to their size.
theorem
CofiniteTopology.isOpen_iff
{α : Type u}
{s : Set (CofiniteTopology α)}
:
IsOpen s ↔ Set.Nonempty s → Set.Finite sᶜ
theorem
CofiniteTopology.isClosed_iff
{α : Type u}
{s : Set (CofiniteTopology α)}
:
IsClosed s ↔ s = Set.univ ∨ Set.Finite s
theorem
CofiniteTopology.mem_nhds_iff
{α : Type u}
{a : CofiniteTopology α}
{s : Set (CofiniteTopology α)}
:
@[simp]
theorem
continuous_prod_mk
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → β}
{g : α → γ}
:
(Continuous fun x => (f x, g x)) ↔ Continuous f ∧ Continuous g
theorem
continuous_fst
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
Continuous Prod.fst
theorem
Continuous.fst
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → β × γ}
(hf : Continuous f)
:
Continuous fun a => (f a).fst
Postcomposing f with Prod.fst is continuous
theorem
Continuous.fst'
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → γ}
(hf : Continuous f)
:
Continuous fun x => f x.fst
Precomposing f with Prod.fst is continuous
theorem
continuousAt_fst
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{p : α × β}
:
ContinuousAt Prod.fst p
theorem
ContinuousAt.fst
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → β × γ}
{x : α}
(hf : ContinuousAt f x)
:
ContinuousAt (fun a => (f a).fst) x
Postcomposing f with Prod.fst is continuous at x
theorem
ContinuousAt.fst'
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → γ}
{x : α}
{y : β}
(hf : ContinuousAt f x)
:
ContinuousAt (fun x => f x.fst) (x, y)
Precomposing f with Prod.fst is continuous at (x, y)
theorem
ContinuousAt.fst''
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → γ}
{x : α × β}
(hf : ContinuousAt f x.fst)
:
ContinuousAt (fun x => f x.fst) x
Precomposing f with Prod.fst is continuous at x : α × β
theorem
continuous_snd
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
Continuous Prod.snd
theorem
Continuous.snd
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → β × γ}
(hf : Continuous f)
:
Continuous fun a => (f a).snd
Postcomposing f with Prod.snd is continuous
theorem
Continuous.snd'
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : β → γ}
(hf : Continuous f)
:
Continuous fun x => f x.snd
Precomposing f with Prod.snd is continuous
theorem
continuousAt_snd
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{p : α × β}
:
ContinuousAt Prod.snd p
theorem
ContinuousAt.snd
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → β × γ}
{x : α}
(hf : ContinuousAt f x)
:
ContinuousAt (fun a => (f a).snd) x
Postcomposing f with Prod.snd is continuous at x
theorem
ContinuousAt.snd'
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : β → γ}
{x : α}
{y : β}
(hf : ContinuousAt f y)
:
ContinuousAt (fun x => f x.snd) (x, y)
Precomposing f with Prod.snd is continuous at (x, y)
theorem
ContinuousAt.snd''
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : β → γ}
{x : α × β}
(hf : ContinuousAt f x.snd)
:
ContinuousAt (fun x => f x.snd) x
Precomposing f with Prod.snd is continuous at x : α × β
theorem
Continuous.prod_mk
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : γ → α}
{g : γ → β}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun x => (f x, g x)
theorem
Continuous.Prod.mk
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
(a : α)
:
Continuous fun b => (a, b)
theorem
Continuous.Prod.mk_left
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
(b : β)
:
Continuous fun a => (a, b)
theorem
Continuous.comp₂
{α : Type u}
{β : Type v}
{γ : Type u_1}
{δ : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{g : α × β → γ}
(hg : Continuous g)
{e : δ → α}
(he : Continuous e)
{f : δ → β}
(hf : Continuous f)
:
Continuous fun x => g (e x, f x)
theorem
Continuous.comp₃
{α : Type u}
{β : Type v}
{γ : Type u_1}
{δ : Type u_2}
{ε : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
[TopologicalSpace ε]
{g : α × β × γ → ε}
(hg : Continuous g)
{e : δ → α}
(he : Continuous e)
{f : δ → β}
(hf : Continuous f)
{k : δ → γ}
(hk : Continuous k)
:
Continuous fun x => g (e x, f x, k x)
theorem
Continuous.comp₄
{α : Type u}
{β : Type v}
{γ : Type u_1}
{δ : Type u_2}
{ε : Type u_3}
{ζ : Type u_4}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
[TopologicalSpace ε]
[TopologicalSpace ζ]
{g : α × β × γ × ζ → ε}
(hg : Continuous g)
{e : δ → α}
(he : Continuous e)
{f : δ → β}
(hf : Continuous f)
{k : δ → γ}
(hk : Continuous k)
{l : δ → ζ}
(hl : Continuous l)
:
Continuous fun x => g (e x, f x, k x, l x)
theorem
Continuous.prod_map
{α : Type u}
{β : Type v}
{γ : Type u_1}
{δ : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{f : γ → α}
{g : δ → β}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun x => (f x.fst, g x.snd)
theorem
continuous_inf_dom_left₂
{α : Type u_5}
{β : Type u_6}
{γ : Type u_7}
{f : α → β → γ}
{ta1 : TopologicalSpace α}
{ta2 : TopologicalSpace α}
{tb1 : TopologicalSpace β}
{tb2 : TopologicalSpace β}
{tc1 : TopologicalSpace γ}
(h : Continuous fun p => f p.fst p.snd)
:
Continuous fun p => f p.fst p.snd
A version of continuous_inf_dom_left for binary functions
theorem
continuous_inf_dom_right₂
{α : Type u_5}
{β : Type u_6}
{γ : Type u_7}
{f : α → β → γ}
{ta1 : TopologicalSpace α}
{ta2 : TopologicalSpace α}
{tb1 : TopologicalSpace β}
{tb2 : TopologicalSpace β}
{tc1 : TopologicalSpace γ}
(h : Continuous fun p => f p.fst p.snd)
:
Continuous fun p => f p.fst p.snd
A version of continuous_inf_dom_right for binary functions
theorem
continuous_sInf_dom₂
{α : Type u_5}
{β : Type u_6}
{γ : Type u_7}
{f : α → β → γ}
{tas : Set (TopologicalSpace α)}
{tbs : Set (TopologicalSpace β)}
{ta : TopologicalSpace α}
{tb : TopologicalSpace β}
{tc : TopologicalSpace γ}
(ha : ta ∈ tas)
(hb : tb ∈ tbs)
(hf : Continuous fun p => f p.fst p.snd)
:
Continuous fun p => f p.fst p.snd
A version of continuous_sInf_dom for binary functions
theorem
Filter.Eventually.prod_inl_nhds
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{p : α → Prop}
{a : α}
(h : ∀ᶠ (x : α) in nhds a, p x)
(b : β)
:
theorem
Filter.Eventually.prod_inr_nhds
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{p : β → Prop}
{b : β}
(h : ∀ᶠ (x : β) in nhds b, p x)
(a : α)
:
theorem
Filter.Eventually.prod_mk_nhds
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{pa : α → Prop}
{a : α}
(ha : ∀ᶠ (x : α) in nhds a, pa x)
{pb : β → Prop}
{b : β}
(hb : ∀ᶠ (y : β) in nhds b, pb y)
:
theorem
continuous_swap
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
Continuous Prod.swap
theorem
continuous_uncurry_left
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → β → γ}
(a : α)
(h : Continuous (Function.uncurry f))
:
Continuous (f a)
theorem
continuous_uncurry_right
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → β → γ}
(b : β)
(h : Continuous (Function.uncurry f))
:
Continuous fun a => f a b
theorem
continuous_curry
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{g : α × β → γ}
(a : α)
(h : Continuous g)
:
Continuous (Function.curry g a)
theorem
IsOpen.prod
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set α}
{t : Set β}
(hs : IsOpen s)
(ht : IsOpen t)
:
theorem
nhds_prod_eq
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{a : α}
{b : β}
:
theorem
nhdsWithin_prod_eq
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
(a : α)
(b : β)
(s : Set α)
(t : Set β)
:
nhdsWithin (a, b) (s ×ˢ t) = nhdsWithin a s ×ˢ nhdsWithin b t
theorem
continuous_uncurry_of_discreteTopology
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[DiscreteTopology α]
{f : α → β → γ}
(hf : ∀ (a : α), Continuous (f a))
:
If a function f x y is such that y ↦ f x y is continuous for all x, and x lives in a
discrete space, then f is continuous.
theorem
Filter.HasBasis.prod_nhds
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{ιa : Type u_5}
{ιb : Type u_6}
{pa : ιa → Prop}
{pb : ιb → Prop}
{sa : ιa → Set α}
{sb : ιb → Set β}
{a : α}
{b : β}
(ha : Filter.HasBasis (nhds a) pa sa)
(hb : Filter.HasBasis (nhds b) pb sb)
:
Filter.HasBasis (nhds (a, b)) (fun i => pa i.fst ∧ pb i.snd) fun i => sa i.fst ×ˢ sb i.snd
theorem
Filter.HasBasis.prod_nhds'
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{ιa : Type u_5}
{ιb : Type u_6}
{pa : ιa → Prop}
{pb : ιb → Prop}
{sa : ιa → Set α}
{sb : ιb → Set β}
{ab : α × β}
(ha : Filter.HasBasis (nhds ab.fst) pa sa)
(hb : Filter.HasBasis (nhds ab.snd) pb sb)
:
Filter.HasBasis (nhds ab) (fun i => pa i.fst ∧ pb i.snd) fun i => sa i.fst ×ˢ sb i.snd
theorem
Prod.tendsto_iff
{β : Type v}
{γ : Type u_1}
[TopologicalSpace β]
[TopologicalSpace γ]
{α : Type u_5}
(seq : α → β × γ)
{f : Filter α}
(x : β × γ)
:
Filter.Tendsto seq f (nhds x) ↔ Filter.Tendsto (fun n => (seq n).fst) f (nhds x.fst) ∧ Filter.Tendsto (fun n => (seq n).snd) f (nhds x.snd)
instance
instDiscreteTopologyProdInstTopologicalSpaceProd
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
[DiscreteTopology α]
[DiscreteTopology β]
:
DiscreteTopology (α × β)
theorem
prod_mem_nhds
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set α}
{t : Set β}
{a : α}
{b : β}
(ha : s ∈ nhds a)
(hb : t ∈ nhds b)
:
theorem
Filter.Eventually.prod_nhds
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{p : α → Prop}
{q : β → Prop}
{a : α}
{b : β}
(ha : ∀ᶠ (x : α) in nhds a, p x)
(hb : ∀ᶠ (y : β) in nhds b, q y)
:
theorem
nhds_swap
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
(a : α)
(b : β)
:
nhds (a, b) = Filter.map Prod.swap (nhds (b, a))
theorem
Filter.Tendsto.prod_mk_nhds
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{γ : Type u_5}
{a : α}
{b : β}
{f : Filter γ}
{ma : γ → α}
{mb : γ → β}
(ha : Filter.Tendsto ma f (nhds a))
(hb : Filter.Tendsto mb f (nhds b))
:
Filter.Tendsto (fun c => (ma c, mb c)) f (nhds (a, b))
theorem
Filter.Eventually.curry_nhds
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{p : α × β → Prop}
{x : α}
{y : β}
(h : ∀ᶠ (x : α × β) in nhds (x, y), p x)
:
theorem
ContinuousAt.prod
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → β}
{g : α → γ}
{x : α}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (fun x => (f x, g x)) x
theorem
ContinuousAt.prod_map
{α : Type u}
{β : Type v}
{γ : Type u_1}
{δ : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{f : α → γ}
{g : β → δ}
{p : α × β}
(hf : ContinuousAt f p.fst)
(hg : ContinuousAt g p.snd)
:
ContinuousAt (fun p => (f p.fst, g p.snd)) p
theorem
ContinuousAt.prod_map'
{α : Type u}
{β : Type v}
{γ : Type u_1}
{δ : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{f : α → γ}
{g : β → δ}
{x : α}
{y : β}
(hf : ContinuousAt f x)
(hg : ContinuousAt g y)
:
ContinuousAt (fun p => (f p.fst, g p.snd)) (x, y)
theorem
prod_induced_induced
{α : Type u}
{β : Type v}
{γ : Type u_1}
{δ : Type u_2}
[TopologicalSpace β]
[TopologicalSpace δ]
(f : α → β)
(g : γ → δ)
:
instTopologicalSpaceProd = TopologicalSpace.induced (fun p => (f p.fst, g p.snd)) instTopologicalSpaceProd
A product of induced topologies is induced by the product map
theorem
continuous_uncurry_of_discreteTopology_left
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[DiscreteTopology α]
{f : α → β → γ}
(h : ∀ (a : α), Continuous (f a))
:
theorem
map_fst_nhdsWithin
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
(x : α × β)
:
Filter.map Prod.fst (nhdsWithin x (Prod.snd ⁻¹' {x.snd})) = nhds x.fst
Prod.fst maps neighborhood of x : α × β within the section Prod.snd ⁻¹' {x.2}
to 𝓝 x.1.
@[simp]
theorem
map_fst_nhds
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
(x : α × β)
:
Filter.map Prod.fst (nhds x) = nhds x.fst
theorem
isOpenMap_fst
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
IsOpenMap Prod.fst
The first projection in a product of topological spaces sends open sets to open sets.
theorem
map_snd_nhdsWithin
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
(x : α × β)
:
Filter.map Prod.snd (nhdsWithin x (Prod.fst ⁻¹' {x.fst})) = nhds x.snd
Prod.snd maps neighborhood of x : α × β within the section Prod.fst ⁻¹' {x.1}
to 𝓝 x.2.
@[simp]
theorem
map_snd_nhds
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
(x : α × β)
:
Filter.map Prod.snd (nhds x) = nhds x.snd
theorem
isOpenMap_snd
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
IsOpenMap Prod.snd
The second projection in a product of topological spaces sends open sets to open sets.
theorem
closure_prod_eq
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set α}
{t : Set β}
:
theorem
interior_prod_eq
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
(s : Set α)
(t : Set β)
:
@[simp]
theorem
frontier_prod_univ_eq
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
(s : Set α)
:
@[simp]
theorem
frontier_univ_prod_eq
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
(s : Set β)
:
theorem
map_mem_closure₂
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → β → γ}
{a : α}
{b : β}
{s : Set α}
{t : Set β}
{u : Set γ}
(hf : Continuous (Function.uncurry f))
(ha : a ∈ closure s)
(hb : b ∈ closure t)
(h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a b ∈ u)
:
theorem
IsClosed.prod
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{s₁ : Set α}
{s₂ : Set β}
(h₁ : IsClosed s₁)
(h₂ : IsClosed s₂)
:
theorem
Dense.prod
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set α}
{t : Set β}
(hs : Dense s)
(ht : Dense t)
:
The product of two dense sets is a dense set.
theorem
DenseRange.prod_map
{β : Type v}
{γ : Type u_1}
[TopologicalSpace β]
[TopologicalSpace γ]
{ι : Type u_5}
{κ : Type u_6}
{f : ι → β}
{g : κ → γ}
(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.
theorem
Inducing.prod_map
{α : Type u}
{β : Type v}
{γ : Type u_1}
{δ : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{f : α → β}
{g : γ → δ}
(hf : Inducing f)
(hg : Inducing g)
:
@[simp]
theorem
inducing_const_prod
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{a : α}
{f : β → γ}
:
@[simp]
theorem
inducing_prod_const
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{b : β}
{f : α → γ}
:
theorem
Embedding.prod_map
{α : Type u}
{β : Type v}
{γ : Type u_1}
{δ : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{f : α → β}
{g : γ → δ}
(hf : Embedding f)
(hg : Embedding g)
:
theorem
IsOpenMap.prod
{α : Type u}
{β : Type v}
{γ : Type u_1}
{δ : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{f : α → β}
{g : γ → δ}
(hf : IsOpenMap f)
(hg : IsOpenMap g)
:
IsOpenMap fun p => (f p.fst, g p.snd)
theorem
OpenEmbedding.prod
{α : Type u}
{β : Type v}
{γ : Type u_1}
{δ : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{f : α → β}
{g : γ → δ}
(hf : OpenEmbedding f)
(hg : OpenEmbedding g)
:
OpenEmbedding fun x => (f x.fst, g x.snd)
theorem
embedding_graph
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : Continuous f)
:
Embedding fun x => (x, f x)
theorem
embedding_prod_mk
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
(x : α)
:
theorem
continuous_sum_dom
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α ⊕ β → γ}
:
Continuous f ↔ Continuous (f ∘ Sum.inl) ∧ Continuous (f ∘ Sum.inr)
theorem
continuous_sum_elim
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → γ}
{g : β → γ}
:
Continuous (Sum.elim f g) ↔ Continuous f ∧ Continuous g
theorem
Continuous.sum_elim
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → γ}
{g : β → γ}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous (Sum.elim f g)
theorem
continuous_isLeft
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
Continuous Sum.isLeft
theorem
continuous_isRight
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
Continuous Sum.isRight
theorem
continuous_inl
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
Continuous Sum.inl
theorem
continuous_inr
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
Continuous Sum.inr
theorem
isOpen_sum_iff
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set (α ⊕ β)}
:
theorem
isClosed_sum_iff
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set (α ⊕ β)}
:
theorem
isOpenMap_inl
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
IsOpenMap Sum.inl
theorem
isOpenMap_inr
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
IsOpenMap Sum.inr
theorem
openEmbedding_inl
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
OpenEmbedding Sum.inl
theorem
openEmbedding_inr
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
OpenEmbedding Sum.inr
theorem
embedding_inl
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
Embedding Sum.inl
theorem
embedding_inr
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
Embedding Sum.inr
theorem
closedEmbedding_inl
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
ClosedEmbedding Sum.inl
theorem
closedEmbedding_inr
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
:
ClosedEmbedding Sum.inr
theorem
nhds_inl
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
(x : α)
:
nhds (Sum.inl x) = Filter.map Sum.inl (nhds x)
theorem
nhds_inr
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
(x : β)
:
nhds (Sum.inr x) = Filter.map Sum.inr (nhds x)
@[simp]
theorem
continuous_sum_map
{α : Type u}
{β : Type v}
{γ : Type u_1}
{δ : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{f : α → β}
{g : γ → δ}
:
Continuous (Sum.map f g) ↔ Continuous f ∧ Continuous g
theorem
Continuous.sum_map
{α : Type u}
{β : Type v}
{γ : Type u_1}
{δ : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{f : α → β}
{g : γ → δ}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous (Sum.map f g)
theorem
isOpenMap_sum
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α ⊕ β → γ}
:
@[simp]
theorem
isOpenMap_sum_elim
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → γ}
{g : β → γ}
:
theorem
IsOpenMap.sum_elim
{α : Type u}
{β : Type v}
{γ : Type u_1}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → γ}
{g : β → γ}
(hf : IsOpenMap f)
(hg : IsOpenMap g)
:
theorem
Inducing.of_codRestrict
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{b : Set β}
(hb : ∀ (a : α), f a ∈ b)
(h : Inducing (Set.codRestrict f b hb))
:
Inducing f
theorem
embedding_subtype_val
{α : Type u}
[TopologicalSpace α]
{p : α → Prop}
:
Embedding Subtype.val
theorem
closedEmbedding_subtype_val
{α : Type u}
[TopologicalSpace α]
{p : α → Prop}
(h : IsClosed {a | p a})
:
ClosedEmbedding Subtype.val
theorem
continuous_subtype_val
{α : Type u}
[TopologicalSpace α]
{p : α → Prop}
:
Continuous Subtype.val
theorem
Continuous.subtype_val
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{p : α → Prop}
{f : β → Subtype p}
(hf : Continuous f)
:
Continuous fun x => ↑(f x)
theorem
IsOpen.openEmbedding_subtype_val
{α : Type u}
[TopologicalSpace α]
{s : Set α}
(hs : IsOpen s)
:
OpenEmbedding Subtype.val
theorem
IsOpen.isOpenMap_subtype_val
{α : Type u}
[TopologicalSpace α]
{s : Set α}
(hs : IsOpen s)
:
IsOpenMap Subtype.val
theorem
IsOpenMap.restrict
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hf : IsOpenMap f)
{s : Set α}
(hs : IsOpen s)
:
IsOpenMap (Set.restrict s f)
theorem
IsClosedMap.restrictPreimage
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
(hcl : IsClosedMap f)
(T : Set β)
:
theorem
IsClosed.closedEmbedding_subtype_val
{α : Type u}
[TopologicalSpace α]
{s : Set α}
(hs : IsClosed s)
:
ClosedEmbedding Subtype.val
theorem
Continuous.subtype_mk
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{p : α → Prop}
{f : β → α}
(h : Continuous f)
(hp : (x : β) → p (f x))
:
Continuous fun x => { val := f x, property := hp x }
theorem
Continuous.subtype_map
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{p : α → Prop}
{f : α → β}
(h : Continuous f)
{q : β → Prop}
(hpq : (x : α) → p x → q (f x))
:
Continuous (Subtype.map f hpq)
theorem
continuous_inclusion
{α : Type u}
[TopologicalSpace α]
{s : Set α}
{t : Set α}
(h : s ⊆ t)
:
theorem
continuousAt_subtype_val
{α : Type u}
[TopologicalSpace α]
{p : α → Prop}
{a : Subtype p}
:
ContinuousAt Subtype.val a
theorem
map_nhds_subtype_val
{α : Type u}
[TopologicalSpace α]
{s : Set α}
(a : ↑s)
:
Filter.map Subtype.val (nhds a) = nhdsWithin (↑a) s
theorem
map_nhds_subtype_coe_eq_nhds
{α : Type u}
[TopologicalSpace α]
{p : α → Prop}
{a : α}
(ha : p a)
(h : ∀ᶠ (x : α) in nhds a, p x)
:
Filter.map Subtype.val (nhds { val := a, property := ha }) = nhds a
theorem
nhds_subtype_eq_comap
{α : Type u}
[TopologicalSpace α]
{p : α → Prop}
{a : α}
{h : p a}
:
nhds { val := a, property := h } = Filter.comap Subtype.val (nhds a)
theorem
tendsto_subtype_rng
{α : Type u}
[TopologicalSpace α]
{β : Type u_5}
{p : α → Prop}
{b : Filter β}
{f : β → Subtype p}
{a : Subtype p}
:
Filter.Tendsto f b (nhds a) ↔ Filter.Tendsto (fun x => ↑(f x)) b (nhds ↑a)
@[simp]
theorem
continuousAt_codRestrict_iff
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{t : Set β}
(h1 : ∀ (x : α), f x ∈ t)
{x : α}
:
ContinuousAt (Set.codRestrict f t h1) x ↔ ContinuousAt f x
theorem
ContinuousAt.codRestrict
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{t : Set β}
(h1 : ∀ (x : α), f x ∈ t)
{x : α}
:
ContinuousAt f x → ContinuousAt (Set.codRestrict f t h1) x
Alias of the reverse direction of continuousAt_codRestrict_iff.
theorem
ContinuousAt.restrict
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{s : Set α}
{t : Set β}
(h1 : Set.MapsTo f s t)
{x : ↑s}
(h2 : ContinuousAt f ↑x)
:
ContinuousAt (Set.MapsTo.restrict f s t h1) x
theorem
ContinuousAt.restrictPreimage
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{s : Set β}
{x : ↑(f ⁻¹' s)}
(h : ContinuousAt f ↑x)
:
ContinuousAt (Set.restrictPreimage s f) x
theorem
Continuous.codRestrict
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{s : Set β}
(hf : Continuous f)
(hs : ∀ (a : α), f a ∈ s)
:
Continuous (Set.codRestrict f s hs)
theorem
Continuous.restrict
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{s : Set α}
{t : Set β}
(h1 : Set.MapsTo f s t)
(h2 : Continuous f)
:
Continuous (Set.MapsTo.restrict f s t h1)
theorem
Continuous.restrictPreimage
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{s : Set β}
(h : Continuous f)
:
theorem
Inducing.codRestrict
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{e : α → β}
(he : Inducing e)
{s : Set β}
(hs : ∀ (x : α), e x ∈ s)
:
Inducing (Set.codRestrict e s hs)
theorem
Embedding.codRestrict
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{e : α → β}
(he : Embedding e)
(s : Set β)
(hs : ∀ (x : α), e x ∈ s)
:
Embedding (Set.codRestrict e s hs)
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
quotientMap_quot_mk
{α : Type u}
[TopologicalSpace α]
{r : α → α → Prop}
:
QuotientMap (Quot.mk r)
theorem
continuous_quot_mk
{α : Type u}
[TopologicalSpace α]
{r : α → α → Prop}
:
Continuous (Quot.mk r)
theorem
continuous_quot_lift
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{r : α → α → Prop}
{f : α → β}
(hr : ∀ (a b : α), r a b → f a = f b)
(h : Continuous f)
:
Continuous (Quot.lift f hr)
theorem
quotientMap_quotient_mk'
{α : Type u}
[TopologicalSpace α]
{s : Setoid α}
:
QuotientMap Quotient.mk'
theorem
continuous_quotient_mk'
{α : Type u}
[TopologicalSpace α]
{s : Setoid α}
:
Continuous Quotient.mk'
theorem
Continuous.quotient_lift
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Setoid α}
{f : α → β}
(h : Continuous f)
(hs : ∀ (a b : α), a ≈ b → f a = f b)
:
Continuous (Quotient.lift f hs)
theorem
Continuous.quotient_liftOn'
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Setoid α}
{f : α → β}
(h : Continuous f)
(hs : ∀ (a b : α), Setoid.r a b → f a = f b)
:
Continuous fun x => Quotient.liftOn' x f hs
theorem
Continuous.quotient_map'
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Setoid α}
{t : Setoid β}
{f : α → β}
(hf : Continuous f)
(H : (Setoid.r ⇒ Setoid.r) f f)
:
Continuous (Quotient.map' f H)
theorem
continuous_pi_iff
{α : Type u}
{ι : Type u_5}
{π : ι → Type u_6}
[TopologicalSpace α]
[T : (i : ι) → TopologicalSpace (π i)]
{f : α → (i : ι) → π i}
:
Continuous f ↔ ∀ (i : ι), Continuous fun a => f a i
theorem
continuous_pi
{α : Type u}
{ι : Type u_5}
{π : ι → Type u_6}
[TopologicalSpace α]
[T : (i : ι) → TopologicalSpace (π i)]
{f : α → (i : ι) → π i}
(h : ∀ (i : ι), Continuous fun a => f a i)
:
theorem
continuous_apply
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
(i : ι)
:
Continuous fun p => 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 => p j i
theorem
continuousAt_apply
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
(i : ι)
(x : (i : ι) → π i)
:
ContinuousAt (fun p => p i) x
theorem
Filter.Tendsto.apply
{β : Type v}
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{l : Filter β}
{f : β → (i : ι) → π i}
{x : (i : ι) → π i}
(h : Filter.Tendsto f l (nhds x))
(i : ι)
:
Filter.Tendsto (fun a => f a i) l (nhds (x i))
theorem
tendsto_pi_nhds
{β : Type v}
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{f : β → (i : ι) → π i}
{g : (i : ι) → π i}
{u : Filter β}
:
Filter.Tendsto f u (nhds g) ↔ ∀ (x : ι), Filter.Tendsto (fun i => f i x) u (nhds (g x))
theorem
continuousAt_pi
{α : Type u}
{ι : Type u_5}
{π : ι → Type u_6}
[TopologicalSpace α]
[T : (i : ι) → TopologicalSpace (π i)]
{f : α → (i : ι) → π i}
{x : α}
:
ContinuousAt f x ↔ ∀ (i : ι), ContinuousAt (fun y => f y i) x
theorem
Pi.continuous_precomp'
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{ι' : Type u_8}
(φ : ι' → ι)
:
Continuous fun f j => f (φ j)
theorem
Pi.continuous_precomp
{α : Type u}
{ι : Type u_5}
[TopologicalSpace α]
{ι' : Type u_8}
(φ : ι' → ι)
:
Continuous fun x => x ∘ φ
theorem
Pi.continuous_postcomp'
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{ρ : ι → Type u_8}
[(i : ι) → TopologicalSpace (ρ i)]
{g : (i : ι) → π i → ρ i}
(hg : ∀ (i : ι), Continuous (g i))
:
Continuous fun f i => g i (f i)
theorem
Pi.continuous_postcomp
{α : Type u}
{β : Type v}
{ι : Type u_5}
[TopologicalSpace α]
[TopologicalSpace β]
{g : α → β}
(hg : Continuous g)
:
Continuous fun x => g ∘ x
theorem
Pi.induced_precomp'
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{ι' : Type u_8}
(φ : ι' → ι)
:
TopologicalSpace.induced (fun f j => f (φ j)) Pi.topologicalSpace = ⨅ (i' : ι'), TopologicalSpace.induced (Function.eval (φ i')) (T (φ i'))
theorem
Pi.induced_precomp
{β : Type v}
{ι : Type u_5}
[TopologicalSpace β]
{ι' : Type u_8}
(φ : ι' → ι)
:
TopologicalSpace.induced (fun x => 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 ι)
:
theorem
Pi.induced_restrict
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
(S : Set ι)
:
TopologicalSpace.induced (Set.restrict S) Pi.topologicalSpace = ⨅ (i : ι) (_ : i ∈ S), TopologicalSpace.induced (Function.eval i) (T i)
theorem
Filter.Tendsto.update
{β : Type v}
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
[DecidableEq ι]
{l : Filter β}
{f : β → (i : ι) → π i}
{x : (i : ι) → π i}
(hf : Filter.Tendsto f l (nhds x))
(i : ι)
{g : β → π i}
{xi : π i}
(hg : Filter.Tendsto g l (nhds xi))
:
Filter.Tendsto (fun a => Function.update (f a) i (g a)) l (nhds (Function.update x i xi))
theorem
ContinuousAt.update
{α : Type u}
{ι : Type u_5}
{π : ι → Type u_6}
[TopologicalSpace α]
[T : (i : ι) → TopologicalSpace (π i)]
{f : α → (i : ι) → π i}
[DecidableEq ι]
{a : α}
(hf : ContinuousAt f a)
(i : ι)
{g : α → π i}
(hg : ContinuousAt g a)
:
ContinuousAt (fun a => Function.update (f a) i (g a)) a
theorem
Continuous.update
{α : Type u}
{ι : Type u_5}
{π : ι → Type u_6}
[TopologicalSpace α]
[T : (i : ι) → TopologicalSpace (π i)]
{f : α → (i : ι) → π i}
[DecidableEq ι]
(hf : Continuous f)
(i : ι)
{g : α → π i}
(hg : Continuous g)
:
Continuous fun a => 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 => Function.update f.fst i f.snd
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 => 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 => Pi.mulSingle i x
Pi.mulSingle i x is continuous in x.
theorem
Filter.Tendsto.fin_insertNth
{β : Type v}
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
(i : Fin (n + 1))
{f : β → π i}
{l : Filter β}
{x : π i}
(hf : Filter.Tendsto f l (nhds x))
{g : β → (j : Fin n) → π (Fin.succAbove i j)}
{y : (j : Fin n) → π (Fin.succAbove i j)}
(hg : Filter.Tendsto g l (nhds y))
:
Filter.Tendsto (fun a => Fin.insertNth i (f a) (g a)) l (nhds (Fin.insertNth i x y))
theorem
ContinuousAt.fin_insertNth
{α : Type u}
[TopologicalSpace α]
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
(i : Fin (n + 1))
{f : α → π i}
{a : α}
(hf : ContinuousAt f a)
{g : α → (j : Fin n) → π (Fin.succAbove i j)}
(hg : ContinuousAt g a)
:
ContinuousAt (fun a => Fin.insertNth i (f a) (g a)) a
theorem
Continuous.fin_insertNth
{α : Type u}
[TopologicalSpace α]
{n : ℕ}
{π : Fin (n + 1) → Type u_8}
[(i : Fin (n + 1)) → TopologicalSpace (π i)]
(i : Fin (n + 1))
{f : α → π i}
(hf : Continuous f)
{g : α → (j : Fin n) → π (Fin.succAbove i j)}
(hg : Continuous g)
:
Continuous fun a => Fin.insertNth i (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 : Set.Finite i)
(hs : ∀ (a : ι), a ∈ i → IsOpen (s a))
:
theorem
set_pi_mem_nhds
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{i : Set ι}
{s : (a : ι) → Set (π a)}
{x : (a : ι) → π a}
(hi : Set.Finite i)
(hs : ∀ (a : ι), a ∈ i → s a ∈ nhds (x a))
:
theorem
set_pi_mem_nhds_iff
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{I : Set ι}
(hI : Set.Finite I)
{s : (i : ι) → Set (π i)}
(a : (i : ι) → π i)
:
theorem
interior_pi_set
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
{I : Set ι}
(hI : Set.Finite I)
{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)
:
∃ I, Finset.piecewise I x y ∈ s
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 => 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)
:
Inducing fun x i => f i x
Suppose π i is a family of topological spaces indexed by i : ι, and X is a type
endowed with a family of maps f i : X → π i for every i : ι, hence inducing a
map g : X → Π i, π i. This lemma shows that infimum of the topologies on X induced by
the f i as i : ι varies is simply the topology on X induced by g : X → Π i, π i
where Π i, π i is endowed with the usual product topology.
instance
Pi.discreteTopology
{ι : Type u_5}
{π : ι → Type u_6}
[T : (i : ι) → TopologicalSpace (π i)]
[Finite ι]
[∀ (i : ι), DiscreteTopology (π i)]
:
DiscreteTopology ((i : ι) → π i)
A finite product of discrete spaces is discrete.
theorem
continuous_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
Continuous (Sigma.mk i)
theorem
isOpenMap_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
theorem
isOpen_range_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
theorem
isClosedMap_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
IsClosedMap (Sigma.mk i)
theorem
isClosed_range_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
theorem
openEmbedding_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
theorem
closedEmbedding_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
theorem
embedding_sigmaMk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
{i : ι}
:
theorem
Sigma.nhds_mk
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
(i : ι)
(x : σ i)
:
nhds { fst := i, snd := 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 { fst := i, snd := x }) = nhds x
theorem
isOpen_sigma_fst_preimage
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
(s : Set ι)
:
@[simp]
theorem
continuous_sigma_iff
{α : Type u}
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
[TopologicalSpace α]
{f : Sigma σ → α}
:
Continuous f ↔ ∀ (i : ι), Continuous fun a => f { fst := i, snd := a }
A map out of a sum type is continuous iff its restriction to each summand is.
theorem
continuous_sigma
{α : Type u}
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
[TopologicalSpace α]
{f : Sigma σ → α}
(hf : ∀ (i : ι), Continuous fun a => f { fst := i, snd := a })
:
A map out of a sum type is continuous if its restriction to each summand is.
theorem
inducing_sigma
{α : Type u}
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
[TopologicalSpace α]
{f : Sigma σ → α}
:
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
{α : Type u}
{ι : Type u_5}
{σ : ι → Type u_7}
[(i : ι) → TopologicalSpace (σ i)]
[TopologicalSpace α]
{f : Sigma σ → α}
:
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
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₁)
:
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₁)
:
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₁)
:
OpenEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), OpenEmbedding (f₂ i)
theorem
IsOpen.trans
{α : Type u}
[TopologicalSpace α]
{β : Set α}
{γ : Set ↑β}
(hγ : IsOpen γ)
(hβ : IsOpen β)
:
theorem
IsClosed.trans
{α : Type u}
[TopologicalSpace α]
{β : Set α}
{γ : Set ↑β}
(hγ : IsClosed γ)
(hβ : IsClosed β)
: