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
@[protected, instance]
Equations
@[protected, instance]
def
quot.topological_space
{α : Type u}
{r : α → α → Prop}
[t : topological_space α] :
topological_space (quot r)
Equations
- quot.topological_space = topological_space.coinduced (quot.mk r) t
@[protected, instance]
@[protected, instance]
def
prod.topological_space
{α : Type u}
{β : Type v}
[t₁ : topological_space α]
[t₂ : topological_space β] :
topological_space (α × β)
@[protected, instance]
def
sum.topological_space
{α : Type u}
{β : Type v}
[t₁ : topological_space α]
[t₂ : topological_space β] :
topological_space (α ⊕ β)
@[protected, instance]
def
sigma.topological_space
{α : Type u}
{β : α → Type v}
[t₂ : Π (a : α), topological_space (β a)] :
Equations
- sigma.topological_space = ⨆ (a : α), topological_space.coinduced (sigma.mk a) (t₂ a)
@[protected, instance]
def
Pi.topological_space
{α : Type u}
{β : α → Type v}
[t₂ : Π (a : α), topological_space (β a)] :
topological_space (Π (a : α), β a)
Equations
- Pi.topological_space = ⨅ (a : α), topological_space.induced (λ (f : Π (a : α), β a), f a) (t₂ a)
@[protected, instance]
Equations
theorem
quotient.preimage_mem_nhds
{α : Type u}
[topological_space α]
[s : setoid α]
{V : set (quotient s)}
{a : α}
(hs : V ∈ 𝓝 ⟦a⟧) :
quotient.mk ⁻¹' V ∈ 𝓝 a
theorem
dense.quotient
{α : Type u}
[setoid α]
[topological_space α]
{s : set α}
(H : dense s) :
dense (quotient.mk '' s)
The image of a dense set under quotient.mk is a dense set.
theorem
dense_range.quotient
{α : Type u}
{β : Type v}
[setoid α]
[topological_space α]
{f : β → α}
(hf : dense_range f) :
dense_range (quotient.mk ∘ f)
The composition of quotient.mk and a function with dense range has dense range.
@[protected, instance]
def
subtype.discrete_topology
{α : Type u}
{p : α → Prop}
[topological_space α]
[discrete_topology α] :
@[protected, instance]
def
sum.discrete_topology
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[hα : discrete_topology α]
[hβ : discrete_topology β] :
discrete_topology (α ⊕ β)
@[protected, instance]
def
sigma.discrete_topology
{α : Type u}
{β : α → Type v}
[Π (a : α), topological_space (β a)]
[h : ∀ (a : α), discrete_topology (β a)] :
A type synonym equiped with the topology whose open sets are the empty set and the sets with finite complements.
Equations
- cofinite_topology α = α
The identity equivalence between α and cofinite_topology α.
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
- cofinite_topology.topological_space = {is_open := λ (s : set (cofinite_topology α)), s.nonempty → sᶜ.finite, is_open_univ := _, is_open_inter := _, is_open_sUnion := _}
theorem
cofinite_topology.nhds_eq
{α : Type u}
(a : cofinite_topology α) :
𝓝 a = pure a ⊔ filter.cofinite
theorem
cofinite_topology.mem_nhds_iff
{α : Type u}
{a : cofinite_topology α}
{s : set (cofinite_topology α)} :
@[continuity]
theorem
continuous_at_fst
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{p : α × β} :
theorem
continuous.fst
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → β × γ}
(hf : continuous f) :
continuous (λ (a : α), (f a).fst)
theorem
continuous_at.fst
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → β × γ}
{x : α}
(hf : continuous_at f x) :
continuous_at (λ (a : α), (f a).fst) x
@[continuity]
theorem
continuous_at_snd
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{p : α × β} :
theorem
continuous.snd
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → β × γ}
(hf : continuous f) :
continuous (λ (a : α), (f a).snd)
theorem
continuous_at.snd
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → β × γ}
{x : α}
(hf : continuous_at f x) :
continuous_at (λ (a : α), (f a).snd) x
@[continuity]
theorem
continuous.prod_mk
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : γ → α}
{g : γ → β}
(hf : continuous f)
(hg : continuous g) :
continuous (λ (x : γ), (f x, g x))
@[continuity]
theorem
continuous.prod.mk
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(a : α) :
continuous (prod.mk a)
theorem
continuous.prod_map
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{f : γ → α}
{g : δ → β}
(hf : continuous f)
(hg : continuous g) :
continuous (λ (x : γ × δ), (f x.fst, g x.snd))
theorem
continuous_inf_dom_left₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{ta1 ta2 : topological_space α}
{tb1 tb2 : topological_space β}
{tc1 : topological_space γ}
(h : continuous (λ (p : α × β), f p.fst p.snd)) :
continuous (λ (p : α × β), f p.fst p.snd)
A version of continuous_inf_dom_left for binary functions
theorem
continuous_inf_dom_right₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{ta1 ta2 : topological_space α}
{tb1 tb2 : topological_space β}
{tc1 : topological_space γ}
(h : continuous (λ (p : α × β), f p.fst p.snd)) :
continuous (λ (p : α × β), f p.fst p.snd)
A version of continuous_inf_dom_right for binary functions
theorem
continuous_Inf_dom₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{tas : set (topological_space α)}
{tbs : set (topological_space β)}
{ta : topological_space α}
{tb : topological_space β}
{tc : topological_space γ}
(ha : ta ∈ tas)
(hb : tb ∈ tbs)
(hf : continuous (λ (p : α × β), f p.fst p.snd)) :
continuous (λ (p : α × β), f p.fst p.snd)
A version of continuous_Inf_dom for binary functions
theorem
filter.eventually.prod_inl_nhds
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{p : α → Prop}
{a : α}
(h : ∀ᶠ (x : α) in 𝓝 a, p x)
(b : β) :
theorem
filter.eventually.prod_inr_nhds
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{p : β → Prop}
{b : β}
(h : ∀ᶠ (x : β) in 𝓝 b, p x)
(a : α) :
theorem
filter.eventually.prod_mk_nhds
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{pa : α → Prop}
{a : α}
(ha : ∀ᶠ (x : α) in 𝓝 a, pa x)
{pb : β → Prop}
{b : β}
(hb : ∀ᶠ (y : β) in 𝓝 b, pb y) :
theorem
continuous_uncurry_left
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → β → γ}
(a : α)
(h : continuous (function.uncurry f)) :
continuous (f a)
theorem
continuous_uncurry_right
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → β → γ}
(b : β)
(h : continuous (function.uncurry f)) :
continuous (λ (a : α), f a b)
theorem
continuous_curry
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{g : α × β → γ}
(a : α)
(h : continuous g) :
continuous (function.curry g a)
theorem
is_open.prod
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s : set α}
{t : set β}
(hs : is_open s)
(ht : is_open t) :
theorem
nhds_prod_eq
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{a : α}
{b : β} :
theorem
continuous_uncurry_of_discrete_topology
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
[discrete_topology α]
{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
prod.tendsto_iff
{β : Type v}
{γ : Type w}
[topological_space β]
[topological_space γ]
{α : Type u_1}
(seq : α → β × γ)
{f : filter α}
(x : β × γ) :
filter.tendsto seq f (𝓝 x) ↔ filter.tendsto (λ (n : α), (seq n).fst) f (𝓝 x.fst) ∧ filter.tendsto (λ (n : α), (seq n).snd) f (𝓝 x.snd)
theorem
filter.has_basis.prod_nhds
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{ιa : Type u_1}
{ιb : Type u_2}
{pa : ιa → Prop}
{pb : ιb → Prop}
{sa : ιa → set α}
{sb : ιb → set β}
{a : α}
{b : β}
(ha : (𝓝 a).has_basis pa sa)
(hb : (𝓝 b).has_basis pb sb) :
theorem
filter.has_basis.prod_nhds'
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{ιa : Type u_1}
{ιb : Type u_2}
{pa : ιa → Prop}
{pb : ιb → Prop}
{sa : ιa → set α}
{sb : ιb → set β}
{ab : α × β}
(ha : (𝓝 ab.fst).has_basis pa sa)
(hb : (𝓝 ab.snd).has_basis pb sb) :
@[protected, instance]
def
prod.discrete_topology
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[discrete_topology α]
[discrete_topology β] :
discrete_topology (α × β)
theorem
prod_mem_nhds_iff
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s : set α}
{t : set β}
{a : α}
{b : β} :
theorem
prod_is_open.mem_nhds
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s : set α}
{t : set β}
{a : α}
{b : β}
(ha : s ∈ 𝓝 a)
(hb : t ∈ 𝓝 b) :
theorem
nhds_swap
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(a : α)
(b : β) :
𝓝 (a, b) = filter.map prod.swap (𝓝 (b, a))
theorem
filter.tendsto.prod_mk_nhds
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{γ : Type u_1}
{a : α}
{b : β}
{f : filter γ}
{ma : γ → α}
{mb : γ → β}
(ha : filter.tendsto ma f (𝓝 a))
(hb : filter.tendsto mb f (𝓝 b)) :
filter.tendsto (λ (c : γ), (ma c, mb c)) f (𝓝 (a, b))
theorem
filter.eventually.curry_nhds
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{p : α × β → Prop}
{x : α}
{y : β}
(h : ∀ᶠ (x : α × β) in 𝓝 (x, y), p x) :
theorem
continuous_at.prod
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → β}
{g : α → γ}
{x : α}
(hf : continuous_at f x)
(hg : continuous_at g x) :
continuous_at (λ (x : α), (f x, g x)) x
theorem
continuous_at.prod_map
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{f : α → γ}
{g : β → δ}
{p : α × β}
(hf : continuous_at f p.fst)
(hg : continuous_at g p.snd) :
continuous_at (λ (p : α × β), (f p.fst, g p.snd)) p
theorem
continuous_at.prod_map'
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{f : α → γ}
{g : β → δ}
{x : α}
{y : β}
(hf : continuous_at f x)
(hg : continuous_at g y) :
continuous_at (λ (p : α × β), (f p.fst, g p.snd)) (x, y)
theorem
prod_eq_generate_from
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β] :
theorem
prod_induced_induced
{β : Type v}
{δ : Type x}
[topological_space β]
[topological_space δ]
{α : Type u_1}
{γ : Type u_2}
(f : α → β)
(g : γ → δ) :
prod.topological_space = topological_space.induced (λ (p : α × γ), (f p.fst, g p.snd)) prod.topological_space
A product of induced topologies is induced by the product map
theorem
continuous_uncurry_of_discrete_topology_left
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
[discrete_topology α]
{f : α → β → γ}
(h : ∀ (a : α), continuous (f a)) :
theorem
map_fst_nhds_within
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(x : α × β) :
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}
[topological_space α]
[topological_space β]
(x : α × β) :
The first projection in a product of topological spaces sends open sets to open sets.
theorem
map_snd_nhds_within
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(x : α × β) :
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}
[topological_space α]
[topological_space β]
(x : α × β) :
The second projection in a product of topological spaces sends open sets to open sets.
theorem
closure_prod_eq
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s : set α}
{t : set β} :
theorem
interior_prod_eq
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(s : set α)
(t : set β) :
@[simp]
theorem
frontier_prod_univ_eq
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(s : set α) :
@[simp]
theorem
frontier_univ_prod_eq
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(s : set β) :
theorem
map_mem_closure2
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{s : set α}
{t : set β}
{u : set γ}
{f : α → β → γ}
{a : α}
{b : β}
(hf : continuous (λ (p : α × β), f p.fst p.snd))
(ha : a ∈ closure s)
(hb : b ∈ closure t)
(hu : ∀ (a : α) (b : β), a ∈ s → b ∈ t → f a b ∈ u) :
theorem
is_closed.prod
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s₁ : set α}
{s₂ : set β}
(h₁ : is_closed s₁)
(h₂ : is_closed s₂) :
theorem
dense.prod
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s : set α}
{t : set β}
(hs : dense s)
(ht : dense t) :
The product of two dense sets is a dense set.
theorem
dense_range.prod_map
{β : Type v}
{γ : Type w}
[topological_space β]
[topological_space γ]
{ι : Type u_1}
{κ : Type u_2}
{f : ι → β}
{g : κ → γ}
(hf : dense_range f)
(hg : dense_range g) :
dense_range (prod.map f g)
If f and g are maps with dense range, then prod.map f g has dense range.
theorem
inducing.prod_mk
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{f : α → β}
{g : γ → δ}
(hf : inducing f)
(hg : inducing g) :
theorem
embedding.prod_mk
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{f : α → β}
{g : γ → δ}
(hf : embedding f)
(hg : embedding g) :
@[protected]
theorem
is_open_map.prod
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{f : α → β}
{g : γ → δ}
(hf : is_open_map f)
(hg : is_open_map g) :
is_open_map (λ (p : α × γ), (f p.fst, g p.snd))
@[protected]
theorem
open_embedding.prod
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{f : α → β}
{g : γ → δ}
(hf : open_embedding f)
(hg : open_embedding g) :
open_embedding (λ (x : α × γ), (f x.fst, g x.snd))
theorem
embedding_graph
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{f : α → β}
(hf : continuous f) :
embedding (λ (x : α), (x, f x))
@[continuity]
@[continuity]
@[continuity]
theorem
continuous_sum_rec
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → γ}
{g : β → γ}
(hf : continuous f)
(hg : continuous g) :
continuous (sum.rec f g)
theorem
is_open_sum_iff
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s : set (α ⊕ β)} :
theorem
is_open_map_sum
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α ⊕ β → γ}
(h₁ : is_open_map (λ (a : α), f (sum.inl a)))
(h₂ : is_open_map (λ (b : β), f (sum.inr b))) :
theorem
closed_embedding_inl
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β] :
theorem
closed_embedding_inr
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β] :
theorem
inducing.of_cod_restrict
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{f : α → β}
{b : set β}
(hb : ∀ (a : α), f a ∈ b)
(h : inducing (set.cod_restrict f b hb)) :
inducing f
theorem
closed_embedding_subtype_coe
{α : Type u}
[topological_space α]
{p : α → Prop}
(h : is_closed {a : α | p a}) :
@[continuity]
theorem
continuous.subtype_coe
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{p : α → Prop}
{f : β → subtype p}
(hf : continuous f) :
continuous (λ (x : β), ↑(f x))
theorem
is_open.open_embedding_subtype_coe
{α : Type u}
[topological_space α]
{s : set α}
(hs : is_open s) :
theorem
is_open.is_open_map_subtype_coe
{α : Type u}
[topological_space α]
{s : set α}
(hs : is_open s) :
theorem
is_open_map.restrict
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{f : α → β}
(hf : is_open_map f)
{s : set α}
(hs : is_open s) :
is_open_map (s.restrict f)
theorem
is_closed.closed_embedding_subtype_coe
{α : Type u}
[topological_space α]
{s : set α}
(hs : is_closed s) :
@[continuity]
theorem
continuous_subtype_mk
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{p : α → Prop}
{f : β → α}
(hp : ∀ (x : β), p (f x))
(h : continuous f) :
continuous (λ (x : β), ⟨f x, _⟩)
theorem
continuous_at_subtype_coe
{α : Type u}
[topological_space α]
{p : α → Prop}
{a : subtype p} :
theorem
map_nhds_subtype_coe_eq
{α : Type u}
[topological_space α]
{p : α → Prop}
{a : α}
(ha : p a)
(h : {a : α | p a} ∈ 𝓝 a) :
theorem
tendsto_subtype_rng
{α : Type u}
[topological_space α]
{β : Type u_1}
{p : α → Prop}
{b : filter β}
{f : β → subtype p}
{a : subtype p} :
filter.tendsto f b (𝓝 a) ↔ filter.tendsto (λ (x : β), ↑(f x)) b (𝓝 ↑a)
theorem
continuous_subtype_nhds_cover
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{ι : Sort u_1}
{f : α → β}
{c : ι → α → Prop}
(c_cover : ∀ (x : α), ∃ (i : ι), {x : α | c i x} ∈ 𝓝 x)
(f_cont : ∀ (i : ι), continuous (λ (x : subtype (c i)), f ↑x)) :
theorem
continuous_subtype_is_closed_cover
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{ι : Type u_1}
{f : α → β}
(c : ι → α → Prop)
(h_lf : locally_finite (λ (i : ι), {x : α | c i x}))
(h_is_closed : ∀ (i : ι), is_closed {x : α | c i x})
(h_cover : ∀ (x : α), ∃ (i : ι), c i x)
(f_cont : ∀ (i : ι), continuous (λ (x : subtype (c i)), f ↑x)) :
@[continuity]
theorem
continuous.cod_restrict
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set β}
(hf : continuous f)
(hs : ∀ (a : α), f a ∈ s) :
continuous (set.cod_restrict f s hs)
theorem
inducing.cod_restrict
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{e : α → β}
(he : inducing e)
{s : set β}
(hs : ∀ (x : α), e x ∈ s) :
inducing (set.cod_restrict e s hs)
theorem
embedding.cod_restrict
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{e : α → β}
(he : embedding e)
(s : set β)
(hs : ∀ (x : α), e x ∈ s) :
embedding (set.cod_restrict e s hs)
theorem
quotient_map_quot_mk
{α : Type u}
[topological_space α]
{r : α → α → Prop} :
quotient_map (quot.mk r)
@[continuity]
theorem
continuous_quot_mk
{α : Type u}
[topological_space α]
{r : α → α → Prop} :
continuous (quot.mk r)
@[continuity]
theorem
continuous_quot_lift
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{r : α → α → Prop}
{f : α → β}
(hr : ∀ (a b : α), r a b → f a = f b)
(h : continuous f) :
continuous (quot.lift f hr)
theorem
continuous_quotient_lift
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s : setoid α}
{f : α → β}
(hs : ∀ (a b : α), a ≈ b → f a = f b)
(h : continuous f) :
continuous (quotient.lift f hs)
theorem
continuous_quotient_lift_on'
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s : setoid α}
{f : α → β}
(hs : ∀ (a b : α), a ≈ b → f a = f b)
(h : continuous f) :
continuous (λ (x : quotient s), x.lift_on' f hs)
@[continuity]
theorem
continuous_pi
{α : Type u}
{ι : Type u_1}
{π : ι → Type u_2}
[topological_space α]
[Π (i : ι), topological_space (π i)]
{f : α → Π (i : ι), π i}
(h : ∀ (i : ι), continuous (λ (a : α), f a i)) :
@[continuity]
theorem
continuous_apply
{ι : Type u_1}
{π : ι → Type u_2}
[Π (i : ι), topological_space (π i)]
(i : ι) :
continuous (λ (p : Π (i : ι), π i), p i)
@[continuity]
theorem
continuous_apply_apply
{ι : Type u_1}
{κ : Type u_2}
{ρ : κ → ι → Type u_3}
[Π (j : κ) (i : ι), topological_space (ρ j i)]
(j : κ)
(i : ι) :
continuous (λ (p : Π (j : κ) (i : ι), ρ j i), p j i)
theorem
continuous_at_apply
{ι : Type u_1}
{π : ι → Type u_2}
[Π (i : ι), topological_space (π i)]
(i : ι)
(x : Π (i : ι), π i) :
continuous_at (λ (p : Π (i : ι), π i), p i) x
theorem
filter.tendsto.apply
{α : Type u}
{ι : Type u_1}
{π : ι → Type u_2}
[Π (i : ι), topological_space (π i)]
{l : filter α}
{f : α → Π (i : ι), π i}
{x : Π (i : ι), π i}
(h : filter.tendsto f l (𝓝 x))
(i : ι) :
filter.tendsto (λ (a : α), f a i) l (𝓝 (x i))
theorem
continuous_pi_iff
{α : Type u}
{ι : Type u_1}
{π : ι → Type u_2}
[topological_space α]
[Π (i : ι), topological_space (π i)]
{f : α → Π (i : ι), π i} :
continuous f ↔ ∀ (i : ι), continuous (λ (y : α), f y i)
theorem
tendsto_pi_nhds
{α : Type u}
{ι : Type u_1}
{π : ι → Type u_2}
[t : Π (i : ι), topological_space (π i)]
{f : α → Π (i : ι), π i}
{g : Π (i : ι), π i}
{u : filter α} :
filter.tendsto f u (𝓝 g) ↔ ∀ (x : ι), filter.tendsto (λ (i : α), f i x) u (𝓝 (g x))
theorem
continuous_at_pi
{α : Type u}
{ι : Type u_1}
{π : ι → Type u_2}
[Π (i : ι), topological_space (π i)]
[topological_space α]
{f : α → Π (i : ι), π i}
{x : α} :
continuous_at f x ↔ ∀ (i : ι), continuous_at (λ (y : α), f y i) x
theorem
filter.tendsto.update
{α : Type u}
{ι : Type u_1}
{π : ι → Type u_2}
[Π (i : ι), topological_space (π i)]
[decidable_eq ι]
{l : filter α}
{f : α → Π (i : ι), π i}
{x : Π (i : ι), π i}
(hf : filter.tendsto f l (𝓝 x))
(i : ι)
{g : α → π i}
{xi : π i}
(hg : filter.tendsto g l (𝓝 xi)) :
filter.tendsto (λ (a : α), function.update (f a) i (g a)) l (𝓝 (function.update x i xi))
theorem
continuous_at.update
{α : Type u}
{ι : Type u_1}
{π : ι → Type u_2}
[Π (i : ι), topological_space (π i)]
[topological_space α]
[decidable_eq ι]
{f : α → Π (i : ι), π i}
{a : α}
(hf : continuous_at f a)
(i : ι)
{g : α → π i}
(hg : continuous_at g a) :
continuous_at (λ (a : α), function.update (f a) i (g a)) a
theorem
continuous.update
{α : Type u}
{ι : Type u_1}
{π : ι → Type u_2}
[Π (i : ι), topological_space (π i)]
[topological_space α]
[decidable_eq ι]
{f : α → Π (i : ι), π i}
(hf : continuous f)
(i : ι)
{g : α → π i}
(hg : continuous g) :
continuous (λ (a : α), function.update (f a) i (g a))
@[continuity]
theorem
continuous_update
{ι : Type u_1}
{π : ι → Type u_2}
[Π (i : ι), topological_space (π i)]
[decidable_eq ι]
(i : ι) :
continuous (λ (f : (Π (j : ι), π j) × π i), function.update f.fst i f.snd)
function.update f i x is continuous in (f, x).
theorem
filter.tendsto.fin_insert_nth
{α : Type u}
{n : ℕ}
{π : fin (n + 1) → Type u_1}
[Π (i : fin (n + 1)), topological_space (π i)]
(i : fin (n + 1))
{f : α → π i}
{l : filter α}
{x : π i}
(hf : filter.tendsto f l (𝓝 x))
{g : α → Π (j : fin n), π (⇑(i.succ_above) j)}
{y : Π (j : fin n), π (⇑(i.succ_above) j)}
(hg : filter.tendsto g l (𝓝 y)) :
filter.tendsto (λ (a : α), i.insert_nth (f a) (g a)) l (𝓝 (i.insert_nth x y))
theorem
continuous_at.fin_insert_nth
{α : Type u}
{n : ℕ}
{π : fin (n + 1) → Type u_1}
[Π (i : fin (n + 1)), topological_space (π i)]
[topological_space α]
(i : fin (n + 1))
{f : α → π i}
{a : α}
(hf : continuous_at f a)
{g : α → Π (j : fin n), π (⇑(i.succ_above) j)}
(hg : continuous_at g a) :
continuous_at (λ (a : α), i.insert_nth (f a) (g a)) a
theorem
continuous.fin_insert_nth
{α : Type u}
{n : ℕ}
{π : fin (n + 1) → Type u_1}
[Π (i : fin (n + 1)), topological_space (π i)]
[topological_space α]
(i : fin (n + 1))
{f : α → π i}
(hf : continuous f)
{g : α → Π (j : fin n), π (⇑(i.succ_above) j)}
(hg : continuous g) :
continuous (λ (a : α), i.insert_nth (f a) (g a))
theorem
is_open_set_pi
{ι : Type u_1}
{π : ι → Type u_2}
[Π (a : ι), topological_space (π a)]
{i : set ι}
{s : Π (a : ι), set (π a)}
(hi : i.finite)
(hs : ∀ (a : ι), a ∈ i → is_open (s a)) :
theorem
is_closed_set_pi
{ι : Type u_1}
{π : ι → Type u_2}
[Π (a : ι), topological_space (π a)]
{i : set ι}
{s : Π (a : ι), set (π a)}
(hs : ∀ (a : ι), a ∈ i → is_closed (s a)) :
theorem
exists_finset_piecewise_mem_of_mem_nhds
{ι : Type u_1}
{π : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), topological_space (π i)]
{s : set (Π (a : ι), π a)}
{x : Π (a : ι), π a}
(hs : s ∈ 𝓝 x)
(y : Π (a : ι), π a) :
theorem
pi_eq_generate_from
{ι : Type u_1}
{π : ι → Type u_2}
[Π (a : ι), topological_space (π a)] :
theorem
pi_generate_from_eq_fintype
{ι : Type u_1}
{π : ι → Type u_2}
{g : Π (a : ι), set (set (π a))}
[fintype ι]
(hg : ∀ (a : ι), ⋃₀g a = set.univ) :
Pi.topological_space = topological_space.generate_from {t : set (Π (a : ι), π a) | ∃ (s : Π (a : ι), set (π a)), (∀ (a : ι), s a ∈ g a) ∧ t = set.univ.pi s}
theorem
inducing_infi_to_pi
{ι : Type u_1}
{π : ι → Type u_2}
{X : Type u_3}
[Π (i : ι), topological_space (π i)]
(f : Π (i : ι), X → π i) :
inducing (λ (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.
@[protected, instance]
def
Pi.discrete_topology
{ι : Type u_1}
{π : ι → Type u_2}
[fintype ι]
[Π (i : ι), topological_space (π i)]
[∀ (i : ι), discrete_topology (π i)] :
discrete_topology (Π (i : ι), π i)
A finite product of discrete spaces is discrete.
@[continuity]
theorem
continuous_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
continuous (sigma.mk i)
theorem
is_open_sigma_iff
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{s : set (sigma σ)} :
theorem
is_closed_sigma_iff
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{s : set (sigma σ)} :
theorem
is_open_map_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
is_open_map (sigma.mk i)
theorem
is_open_range_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
theorem
is_closed_map_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
theorem
is_closed_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
theorem
open_embedding_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
theorem
closed_embedding_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
theorem
embedding_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
theorem
is_open_sigma_fst_preimage
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
(s : set ι) :
@[continuity]
theorem
continuous_sigma
{β : Type v}
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
[topological_space β]
{f : sigma σ → β}
(h : ∀ (i : ι), continuous (λ (a : σ i), f ⟨i, a⟩)) :
A map out of a sum type is continuous if its restriction to each summand is.
@[continuity]
theorem
continuous_sigma_map
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{κ : Type u_3}
{τ : κ → Type u_4}
[Π (k : κ), topological_space (τ k)]
{f₁ : ι → κ}
{f₂ : Π (i : ι), σ i → τ (f₁ i)}
(hf : ∀ (i : ι), continuous (f₂ i)) :
continuous (sigma.map f₁ f₂)
theorem
is_open_map_sigma
{β : Type v}
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
[topological_space β]
{f : sigma σ → β}
(h : ∀ (i : ι), is_open_map (λ (a : σ i), f ⟨i, a⟩)) :
theorem
embedding_sigma_map
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{τ : ι → Type u_3}
[Π (i : ι), topological_space (τ i)]
{f : Π (i : ι), σ i → τ i}
(hf : ∀ (i : ι), embedding (f i)) :
The sum of embeddings is an embedding.
@[continuity]
@[continuity]
theorem
mem_closure_of_continuous
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{f : α → β}
{a : α}
{s : set α}
{t : set β}
(hf : continuous f)
(ha : a ∈ closure s)
(h : set.maps_to f s (closure t)) :
theorem
mem_closure_of_continuous2
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → β → γ}
{a : α}
{b : β}
{s : set α}
{t : set β}
{u : set γ}
(hf : continuous (λ (p : α × β), f p.fst p.snd))
(ha : a ∈ closure s)
(hb : b ∈ closure t)
(h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a b ∈ closure u) :