Homeomorphisms #

This file defines homeomorphisms between two topological spaces. They are bijections with both directions continuous. We denote homeomorphisms with the notation ≃ₜ.

Main definitions #

Homeomorph α β: The type of homeomorphisms from α to β. This type can be denoted using the following notation: α ≃ₜ β.

Main results #

Pretty much every topological property is preserved under homeomorphisms.
Homeomorph.homeomorphOfContinuousOpen: A continuous bijection that is an open map is a homeomorphism.

source

structure Homeomorph (α : Type u_5) (β : Type u_6) [TopologicalSpace α] [TopologicalSpace β] extends Equiv :

Type (max u_5 u_6)

toFun : α → β
invFun : β → α
left_inv : Function.LeftInverse s.invFun s.toFun
right_inv : Function.RightInverse s.invFun s.toFun
continuous_toFun : Continuous s.toFun
The forward map of a homeomorphism is a continuous function.
continuous_invFun : Continuous s.invFun
The inverse map of a homeomorphism is a continuous function.

Homeomorphism between α and β, also called topological isomorphism

Instances For

source

def «term_≃ₜ_» :

Lean.TrailingParserDescr

Homeomorphism between α and β, also called topological isomorphism

Instances For

source

theorem Homeomorph.toEquiv_injective {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :

Function.Injective Homeomorph.toEquiv

source

instance Homeomorph.instEquivLikeHomeomorph {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :

EquivLike (α ≃ₜ β) α β

source

instance Homeomorph.instCoeFunHomeomorphForAll {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :

CoeFun (α ≃ₜ β) fun x => α → β

source

@[simp]

theorem Homeomorph.homeomorph_mk_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (a : α ≃ β) (b : Continuous a.toFun) (c : Continuous a.invFun) :

↑(Homeomorph.mk a) = ↑a

source

def Homeomorph.symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

β ≃ₜ α

Inverse of a homeomorphism.

Instances For

source

@[simp]

theorem Homeomorph.symm_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

Homeomorph.symm (Homeomorph.symm h) = h

source

def Homeomorph.Simps.symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

β → α

See Note [custom simps projection]

Instances For

source

@[simp]

theorem Homeomorph.coe_toEquiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

↑h.toEquiv = ↑h

source

@[simp]

theorem Homeomorph.coe_symm_toEquiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

↑h.symm = ↑(Homeomorph.symm h)

source

theorem Homeomorph.ext {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {h : α ≃ₜ β} {h' : α ≃ₜ β} (H : ∀ (x : α), ↑h x = ↑h' x) :

h = h'

source

@[simp]

theorem Homeomorph.refl_apply (α : Type u_5) [TopologicalSpace α] :

↑(Homeomorph.refl α) = id

source

def Homeomorph.refl (α : Type u_5) [TopologicalSpace α] :

α ≃ₜ α

Identity map as a homeomorphism.

Instances For

source

def Homeomorph.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h₁ : α ≃ₜ β) (h₂ : β ≃ₜ γ) :

α ≃ₜ γ

Composition of two homeomorphisms.

Instances For

source

@[simp]

theorem Homeomorph.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h₁ : α ≃ₜ β) (h₂ : β ≃ₜ γ) (a : α) :

↑(Homeomorph.trans h₁ h₂) a = ↑h₂ (↑h₁ a)

source

@[simp]

theorem Homeomorph.symm_trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : α ≃ₜ β) (g : β ≃ₜ γ) (a : γ) :

↑(Homeomorph.symm (Homeomorph.trans f g)) a = ↑(Homeomorph.symm f) (↑(Homeomorph.symm g) a)

source

@[simp]

theorem Homeomorph.homeomorph_mk_coe_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (a : α ≃ β) (b : Continuous a.toFun) (c : Continuous a.invFun) :

↑(Homeomorph.symm (Homeomorph.mk a)) = ↑a.symm

source

@[simp]

theorem Homeomorph.refl_symm {α : Type u_1} [TopologicalSpace α] :

Homeomorph.symm (Homeomorph.refl α) = Homeomorph.refl α

source

theorem Homeomorph.continuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

Continuous ↑h

source

theorem Homeomorph.continuous_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

Continuous ↑(Homeomorph.symm h)

source

@[simp]

theorem Homeomorph.apply_symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (x : β) :

↑h (↑(Homeomorph.symm h) x) = x

source

@[simp]

theorem Homeomorph.symm_apply_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (x : α) :

↑(Homeomorph.symm h) (↑h x) = x

source

@[simp]

theorem Homeomorph.self_trans_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

Homeomorph.trans h (Homeomorph.symm h) = Homeomorph.refl α

source

@[simp]

theorem Homeomorph.symm_trans_self {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

Homeomorph.trans (Homeomorph.symm h) h = Homeomorph.refl β

source

theorem Homeomorph.bijective {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

Function.Bijective ↑h

source

theorem Homeomorph.injective {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

Function.Injective ↑h

source

theorem Homeomorph.surjective {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

Function.Surjective ↑h

source

def Homeomorph.changeInv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) (g : β → α) (hg : Function.RightInverse g ↑f) :

α ≃ₜ β

Change the homeomorphism f to make the inverse function definitionally equal to g.

Instances For

source

@[simp]

theorem Homeomorph.symm_comp_self {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

↑(Homeomorph.symm h) ∘ ↑h = id

source

@[simp]

theorem Homeomorph.self_comp_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

↑h ∘ ↑(Homeomorph.symm h) = id

source

@[simp]

theorem Homeomorph.range_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

Set.range ↑h = Set.univ

source

theorem Homeomorph.image_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

Set.image ↑(Homeomorph.symm h) = Set.preimage ↑h

source

theorem Homeomorph.preimage_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

Set.preimage ↑(Homeomorph.symm h) = Set.image ↑h

source

@[simp]

theorem Homeomorph.image_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (s : Set β) :

↑h '' (↑h ⁻¹' s) = s

source

@[simp]

theorem Homeomorph.preimage_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (s : Set α) :

↑h ⁻¹' (↑h '' s) = s

source

theorem Homeomorph.inducing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

Inducing ↑h

source

theorem Homeomorph.induced_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

TopologicalSpace.induced (↑h) inst✝ = inst✝¹

source

theorem Homeomorph.quotientMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

QuotientMap ↑h

source

theorem Homeomorph.coinduced_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

TopologicalSpace.coinduced (↑h) inst✝ = inst✝¹

source

theorem Homeomorph.embedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

Embedding ↑h

source

noncomputable def Homeomorph.ofEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (hf : Embedding f) :

α ≃ₜ ↑(Set.range f)

Homeomorphism given an embedding.

Instances For

source

theorem Homeomorph.secondCountableTopology {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace.SecondCountableTopology β] (h : α ≃ₜ β) :

TopologicalSpace.SecondCountableTopology α

source

theorem Homeomorph.isCompact_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (h : α ≃ₜ β) :

IsCompact (↑h '' s) ↔ IsCompact s

source

theorem Homeomorph.isCompact_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set β} (h : α ≃ₜ β) :

IsCompact (↑h ⁻¹' s) ↔ IsCompact s

source

@[simp]

theorem Homeomorph.isPreconnected_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (h : α ≃ₜ β) :

IsPreconnected (↑h '' s) ↔ IsPreconnected s

source

@[simp]

theorem Homeomorph.isPreconnected_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set β} (h : α ≃ₜ β) :

IsPreconnected (↑h ⁻¹' s) ↔ IsPreconnected s

source

@[simp]

theorem Homeomorph.isConnected_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (h : α ≃ₜ β) :

IsConnected (↑h '' s) ↔ IsConnected s

source

@[simp]

theorem Homeomorph.isConnected_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set β} (h : α ≃ₜ β) :

IsConnected (↑h ⁻¹' s) ↔ IsConnected s

source

@[simp]

theorem Homeomorph.comap_cocompact {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

Filter.comap (↑h) (Filter.cocompact β) = Filter.cocompact α

source

@[simp]

theorem Homeomorph.map_cocompact {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

Filter.map (↑h) (Filter.cocompact α) = Filter.cocompact β

source

theorem Homeomorph.compactSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] (h : α ≃ₜ β) :

CompactSpace β

source

theorem Homeomorph.t0Space {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T0Space α] (h : α ≃ₜ β) :

T0Space β

source

theorem Homeomorph.t1Space {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T1Space α] (h : α ≃ₜ β) :

T1Space β

source

theorem Homeomorph.t2Space {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space α] (h : α ≃ₜ β) :

T2Space β

source

theorem Homeomorph.t3Space {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T3Space α] (h : α ≃ₜ β) :

T3Space β

source

theorem Homeomorph.denseEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

DenseEmbedding ↑h

source

@[simp]

theorem Homeomorph.isOpen_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) {s : Set β} :

IsOpen (↑h ⁻¹' s) ↔ IsOpen s

source

@[simp]

theorem Homeomorph.isOpen_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) {s : Set α} :

IsOpen (↑h '' s) ↔ IsOpen s

source

theorem Homeomorph.isOpenMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

IsOpenMap ↑h

source

@[simp]

theorem Homeomorph.isClosed_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) {s : Set β} :

IsClosed (↑h ⁻¹' s) ↔ IsClosed s

source

@[simp]

theorem Homeomorph.isClosed_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) {s : Set α} :

IsClosed (↑h '' s) ↔ IsClosed s

source

theorem Homeomorph.isClosedMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

IsClosedMap ↑h

source

theorem Homeomorph.openEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

OpenEmbedding ↑h

source

theorem Homeomorph.closedEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) :

ClosedEmbedding ↑h

source

theorem Homeomorph.normalSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NormalSpace α] (h : α ≃ₜ β) :

NormalSpace β

source

theorem Homeomorph.t4Space {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T4Space α] (h : α ≃ₜ β) :

T4Space β

source

theorem Homeomorph.preimage_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (s : Set β) :

↑h ⁻¹' closure s = closure (↑h ⁻¹' s)

source

theorem Homeomorph.image_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (s : Set α) :

↑h '' closure s = closure (↑h '' s)

source

theorem Homeomorph.preimage_interior {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (s : Set β) :

↑h ⁻¹' interior s = interior (↑h ⁻¹' s)

source

theorem Homeomorph.image_interior {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (s : Set α) :

↑h '' interior s = interior (↑h '' s)

source

theorem Homeomorph.preimage_frontier {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (s : Set β) :

↑h ⁻¹' frontier s = frontier (↑h ⁻¹' s)

source

theorem Homeomorph.image_frontier {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (s : Set α) :

↑h '' frontier s = frontier (↑h '' s)

source

theorem HasCompactSupport.comp_homeomorph {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {M : Type u_5} [Zero M] {f : β → M} (hf : HasCompactSupport f) (φ : α ≃ₜ β) :

HasCompactSupport (f ∘ ↑φ)

source

theorem HasCompactMulSupport.comp_homeomorph {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {M : Type u_5} [One M] {f : β → M} (hf : HasCompactMulSupport f) (φ : α ≃ₜ β) :

HasCompactMulSupport (f ∘ ↑φ)

source

@[simp]

theorem Homeomorph.map_nhds_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (x : α) :

Filter.map (↑h) (nhds x) = nhds (↑h x)

source

theorem Homeomorph.symm_map_nhds_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (x : α) :

Filter.map (↑(Homeomorph.symm h)) (nhds (↑h x)) = nhds x

source

theorem Homeomorph.nhds_eq_comap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (x : α) :

nhds x = Filter.comap (↑h) (nhds (↑h x))

source

@[simp]

theorem Homeomorph.comap_nhds_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (y : β) :

Filter.comap (↑h) (nhds y) = nhds (↑(Homeomorph.symm h) y)

source

theorem Homeomorph.locallyConnectedSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [i : LocallyConnectedSpace β] (h : α ≃ₜ β) :

LocallyConnectedSpace α

If the codomain of a homeomorphism is a locally connected space, then the domain is also a locally connected space.

source

def Homeomorph.homeomorphOfContinuousOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ β) (h₁ : Continuous ↑e) (h₂ : IsOpenMap ↑e) :

α ≃ₜ β

If a bijective map e : α ≃ β is continuous and open, then it is a homeomorphism.

Instances For

source

@[simp]

theorem Homeomorph.comp_continuousOn_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) (f : γ → α) (s : Set γ) :

ContinuousOn (↑h ∘ f) s ↔ ContinuousOn f s

source

@[simp]

theorem Homeomorph.comp_continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) {f : γ → α} :

Continuous (↑h ∘ f) ↔ Continuous f

source

@[simp]

theorem Homeomorph.comp_continuous_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) {f : β → γ} :

Continuous (f ∘ ↑h) ↔ Continuous f

source

theorem Homeomorph.comp_continuousAt_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) (f : γ → α) (x : γ) :

ContinuousAt (↑h ∘ f) x ↔ ContinuousAt f x

source

theorem Homeomorph.comp_continuousAt_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) (f : β → γ) (x : α) :

ContinuousAt (f ∘ ↑h) x ↔ ContinuousAt f (↑h x)

source

theorem Homeomorph.comp_continuousWithinAt_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) (f : γ → α) (s : Set γ) (x : γ) :

ContinuousWithinAt f s x ↔ ContinuousWithinAt (↑h ∘ f) s x

source

@[simp]

theorem Homeomorph.comp_isOpenMap_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) {f : γ → α} :

IsOpenMap (↑h ∘ f) ↔ IsOpenMap f

source

@[simp]

theorem Homeomorph.comp_isOpenMap_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) {f : β → γ} :

IsOpenMap (f ∘ ↑h) ↔ IsOpenMap f

source

def Homeomorph.setCongr {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} (h : s = t) :

↑s ≃ₜ ↑t

If two sets are equal, then they are homeomorphic.

Instances For

source

def Homeomorph.sumCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (h₁ : α ≃ₜ β) (h₂ : γ ≃ₜ δ) :

α ⊕ γ ≃ₜ β ⊕ δ

Sum of two homeomorphisms.

Instances For

source

def Homeomorph.prodCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (h₁ : α ≃ₜ β) (h₂ : γ ≃ₜ δ) :

α × γ ≃ₜ β × δ

Product of two homeomorphisms.

Instances For

source

@[simp]

theorem Homeomorph.prodCongr_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (h₁ : α ≃ₜ β) (h₂ : γ ≃ₜ δ) :

Homeomorph.symm (Homeomorph.prodCongr h₁ h₂) = Homeomorph.prodCongr (Homeomorph.symm h₁) (Homeomorph.symm h₂)

source

@[simp]

theorem Homeomorph.coe_prodCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (h₁ : α ≃ₜ β) (h₂ : γ ≃ₜ δ) :

↑(Homeomorph.prodCongr h₁ h₂) = Prod.map ↑h₁ ↑h₂

source

def Homeomorph.prodComm (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] :

α × β ≃ₜ β × α

α × β is homeomorphic to β × α.

Instances For

source

@[simp]

theorem Homeomorph.prodComm_symm (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] :

Homeomorph.symm (Homeomorph.prodComm α β) = Homeomorph.prodComm β α

source

@[simp]

theorem Homeomorph.coe_prodComm (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] :

↑(Homeomorph.prodComm α β) = Prod.swap

source

def Homeomorph.prodAssoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] :

(α × β) × γ ≃ₜ α × β × γ

(α × β) × γ is homeomorphic to α × (β × γ).

Instances For

source

@[simp]

theorem Homeomorph.prodPUnit_apply (α : Type u_1) [TopologicalSpace α] :

↑(Homeomorph.prodPUnit α) = fun p => p.fst

source

def Homeomorph.prodPUnit (α : Type u_1) [TopologicalSpace α] :

α × PUnit.{u_5 + 1} ≃ₜ α

α × {*} is homeomorphic to α.

Instances For

source

def Homeomorph.punitProd (α : Type u_1) [TopologicalSpace α] :

PUnit.{u_5 + 1} × α ≃ₜ α

{*} × α is homeomorphic to α.

Instances For

source

@[simp]

theorem Homeomorph.coe_punitProd (α : Type u_1) [TopologicalSpace α] :

↑(Homeomorph.punitProd α) = Prod.snd

source

@[simp]

theorem Homeomorph.homeomorphOfUnique_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [Unique α] [Unique β] :

∀ (a : α), ↑(Homeomorph.homeomorphOfUnique α β) a = default

source

@[simp]

theorem Homeomorph.homeomorphOfUnique_symm_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [Unique α] [Unique β] :

∀ (a : β), ↑(Homeomorph.symm (Homeomorph.homeomorphOfUnique α β)) a = default

source

def Homeomorph.homeomorphOfUnique (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [Unique α] [Unique β] :

α ≃ₜ β

If both α and β have a unique element, then α ≃ₜ β.

Instances For

source

@[simp]

theorem Homeomorph.piCongrLeft_apply {ι : Type u_5} {ι' : Type u_6} {β : ι' → Type u_7} [(j : ι') → TopologicalSpace (β j)] (e : ι ≃ ι') :

∀ (a : (b : ι) → β (↑e.symm.symm b)) (a_1 : ι'), ↑(Homeomorph.piCongrLeft e) a a_1 = ↑(Equiv.piCongrLeft' β e.symm).symm a a_1

source

@[simp]

theorem Homeomorph.piCongrLeft_toEquiv {ι : Type u_5} {ι' : Type u_6} {β : ι' → Type u_7} [(j : ι') → TopologicalSpace (β j)] (e : ι ≃ ι') :

(Homeomorph.piCongrLeft e).toEquiv = Equiv.piCongrLeft β e

source

def Homeomorph.piCongrLeft {ι : Type u_5} {ι' : Type u_6} {β : ι' → Type u_7} [(j : ι') → TopologicalSpace (β j)] (e : ι ≃ ι') :

((i : ι) → β (↑e i)) ≃ₜ ((j : ι') → β j)

Equiv.piCongrLeft as a homeomorphism: this is the natural homeomorphism Π i, β (e i) ≃ₜ Π j, β j obtained from a bijection ι ≃ ι'.

Instances For

source

@[simp]

theorem Homeomorph.piCongrRight_apply {ι : Type u_5} {β₁ : ι → Type u_6} {β₂ : ι → Type u_7} [(i : ι) → TopologicalSpace (β₁ i)] [(i : ι) → TopologicalSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ₜ β₂ i) (H : (a : ι) → (fun i => β₁ i) a) (a : ι) :

↑(Homeomorph.piCongrRight F) H a = ↑(F a) (H a)

source

@[simp]

theorem Homeomorph.piCongrRight_toEquiv {ι : Type u_5} {β₁ : ι → Type u_6} {β₂ : ι → Type u_7} [(i : ι) → TopologicalSpace (β₁ i)] [(i : ι) → TopologicalSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ₜ β₂ i) :

(Homeomorph.piCongrRight F).toEquiv = Equiv.piCongrRight fun i => (F i).toEquiv

source

def Homeomorph.piCongrRight {ι : Type u_5} {β₁ : ι → Type u_6} {β₂ : ι → Type u_7} [(i : ι) → TopologicalSpace (β₁ i)] [(i : ι) → TopologicalSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ₜ β₂ i) :

((i : ι) → β₁ i) ≃ₜ ((i : ι) → β₂ i)

Equiv.piCongrRight as a homeomorphism: this is the natural homeomorphism Π i, β₁ i ≃ₜ Π j, β₂ i obtained from homeomorphisms β₁ i ≃ₜ β₂ i for each i.

Instances For

source

@[simp]

theorem Homeomorph.piCongrRight_symm {ι : Type u_5} {β₁ : ι → Type u_6} {β₂ : ι → Type u_7} [(i : ι) → TopologicalSpace (β₁ i)] [(i : ι) → TopologicalSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ₜ β₂ i) :

Homeomorph.symm (Homeomorph.piCongrRight F) = Homeomorph.piCongrRight fun i => Homeomorph.symm (F i)

source

@[simp]

theorem Homeomorph.piCongr_toEquiv {ι₁ : Type u_5} {ι₂ : Type u_6} {β₁ : ι₁ → Type u_7} {β₂ : ι₂ → Type u_8} [(i₁ : ι₁) → TopologicalSpace (β₁ i₁)] [(i₂ : ι₂) → TopologicalSpace (β₂ i₂)] (e : ι₁ ≃ ι₂) (F : (i₁ : ι₁) → β₁ i₁ ≃ₜ β₂ (↑e i₁)) :

(Homeomorph.piCongr e F).toEquiv = (Equiv.piCongrRight fun i => (F i).toEquiv).trans (Equiv.piCongrLeft β₂ e)

source

@[simp]

theorem Homeomorph.piCongr_apply {ι₁ : Type u_5} {ι₂ : Type u_6} {β₁ : ι₁ → Type u_7} {β₂ : ι₂ → Type u_8} [(i₁ : ι₁) → TopologicalSpace (β₁ i₁)] [(i₂ : ι₂) → TopologicalSpace (β₂ i₂)] (e : ι₁ ≃ ι₂) (F : (i₁ : ι₁) → β₁ i₁ ≃ₜ β₂ (↑e i₁)) :

∀ (a : (i : ι₁) → β₁ i) (i₂ : ι₂), ↑(Homeomorph.piCongr e F) a i₂ = (_ : ↑e (↑e.symm i₂) = i₂) ▸ ↑(Equiv.piCongrRight fun i => (F i).toEquiv) a (↑e.symm i₂)

source

def Homeomorph.piCongr {ι₁ : Type u_5} {ι₂ : Type u_6} {β₁ : ι₁ → Type u_7} {β₂ : ι₂ → Type u_8} [(i₁ : ι₁) → TopologicalSpace (β₁ i₁)] [(i₂ : ι₂) → TopologicalSpace (β₂ i₂)] (e : ι₁ ≃ ι₂) (F : (i₁ : ι₁) → β₁ i₁ ≃ₜ β₂ (↑e i₁)) :

((i₁ : ι₁) → β₁ i₁) ≃ₜ ((i₂ : ι₂) → β₂ i₂)

Equiv.piCongr as a homeomorphism: this is the natural homeomorphism Π i₁, β₁ i ≃ₜ Π i₂, β₂ i₂ obtained from a bijection ι₁ ≃ ι₂ and homeomorphisms β₁ i₁ ≃ₜ β₂ (e i₁) for each i₁ : ι₁.

Instances For

source

def Homeomorph.ulift {α : Type u} [TopologicalSpace α] :

ULift.{v, u} α ≃ₜ α

ULift α is homeomorphic to α.

Instances For

source

def Homeomorph.sumProdDistrib {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] :

(α ⊕ β) × γ ≃ₜ α × γ ⊕ β × γ

(α ⊕ β) × γ is homeomorphic to α × γ ⊕ β × γ.

Instances For

source

def Homeomorph.prodSumDistrib {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] :

α × (β ⊕ γ) ≃ₜ α × β ⊕ α × γ

α × (β ⊕ γ) is homeomorphic to α × β ⊕ α × γ.

Instances For

source

def Homeomorph.sigmaProdDistrib {β : Type u_2} [TopologicalSpace β] {ι : Type u_5} {σ : ι → Type u_6} [(i : ι) → TopologicalSpace (σ i)] :

((i : ι) × σ i) × β ≃ₜ (i : ι) × σ i × β

(Σ i, σ i) × β is homeomorphic to Σ i, (σ i × β).

Instances For

source

@[simp]

theorem Homeomorph.funUnique_symm_apply (ι : Type u_5) (α : Type u_6) [Unique ι] [TopologicalSpace α] :

↑(Homeomorph.symm (Homeomorph.funUnique ι α)) = fun x b => x

source

@[simp]

theorem Homeomorph.funUnique_apply (ι : Type u_5) (α : Type u_6) [Unique ι] [TopologicalSpace α] :

↑(Homeomorph.funUnique ι α) = fun f => f default

source

def Homeomorph.funUnique (ι : Type u_5) (α : Type u_6) [Unique ι] [TopologicalSpace α] :

(ι → α) ≃ₜ α

If ι has a unique element, then ι → α is homeomorphic to α.

Instances For

source

@[simp]

theorem Homeomorph.piFinTwo_apply (α : Fin 2 → Type u) [(i : Fin 2) → TopologicalSpace (α i)] :

↑(Homeomorph.piFinTwo α) = fun f => (f 0, f 1)

source

@[simp]

theorem Homeomorph.piFinTwo_symm_apply (α : Fin 2 → Type u) [(i : Fin 2) → TopologicalSpace (α i)] :

↑(Homeomorph.symm (Homeomorph.piFinTwo α)) = fun p => Fin.cons p.fst (Fin.cons p.snd finZeroElim)

source

def Homeomorph.piFinTwo (α : Fin 2 → Type u) [(i : Fin 2) → TopologicalSpace (α i)] :

((i : Fin 2) → α i) ≃ₜ α 0 × α 1

Homeomorphism between dependent functions Π i : Fin 2, α i and α 0 × α 1.

Instances For

source

@[simp]

theorem Homeomorph.finTwoArrow_symm_apply {α : Type u_1} [TopologicalSpace α] :

↑(Homeomorph.symm Homeomorph.finTwoArrow) = fun x => ![x.fst, x.snd]

source

@[simp]

theorem Homeomorph.finTwoArrow_apply {α : Type u_1} [TopologicalSpace α] :

↑Homeomorph.finTwoArrow = fun f => (f 0, f 1)

source

def Homeomorph.finTwoArrow {α : Type u_1} [TopologicalSpace α] :

(Fin 2 → α) ≃ₜ α × α

Homeomorphism between α² = Fin 2 → α and α × α.

Instances For

source

@[simp]

theorem Homeomorph.image_apply_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) (s : Set α) (x : ↑s) :

↑(↑(Homeomorph.image e s) x) = ↑e ↑x

source

@[simp]

theorem Homeomorph.image_symm_apply_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) (s : Set α) (y : ↑(↑e.toEquiv '' s)) :

↑(↑(Homeomorph.symm (Homeomorph.image e s)) y) = ↑(Homeomorph.symm e) ↑y

source

def Homeomorph.image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) (s : Set α) :

↑s ≃ₜ ↑(↑e '' s)

A subset of a topological space is homeomorphic to its image under a homeomorphism.

Instances For

source

@[simp]

theorem Homeomorph.Set.univ_apply (α : Type u_5) [TopologicalSpace α] :

↑(Homeomorph.Set.univ α) = Subtype.val

source

@[simp]

theorem Homeomorph.Set.univ_symm_apply_coe (α : Type u_5) [TopologicalSpace α] (a : α) :

↑(↑(Homeomorph.symm (Homeomorph.Set.univ α)) a) = a

source

def Homeomorph.Set.univ (α : Type u_5) [TopologicalSpace α] :

↑Set.univ ≃ₜ α

Set.univ α is homeomorphic to α.

Instances For

source

@[simp]

theorem Homeomorph.Set.prod_symm_apply_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (t : Set β) (x : { a // s a } × { b // t b }) :

↑(↑(Homeomorph.symm (Homeomorph.Set.prod s t)) x) = (↑x.fst, ↑x.snd)

source

@[simp]

theorem Homeomorph.Set.prod_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (t : Set β) (x : { c // s c.fst ∧ t c.snd }) :

↑(Homeomorph.Set.prod s t) x = ({ val := (↑x).fst, property := Equiv.subtypeProdEquivProd.proof_1 x }, { val := (↑x).snd, property := Equiv.subtypeProdEquivProd.proof_2 x })

source

def Homeomorph.Set.prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (t : Set β) :

↑(s ×ˢ t) ≃ₜ ↑s × ↑t

s ×ˢ t is homeomorphic to s × t.

Instances For

source

@[simp]

theorem Homeomorph.piEquivPiSubtypeProd_apply {ι : Type u_5} (p : ι → Prop) (β : ι → Type u_6) [(i : ι) → TopologicalSpace (β i)] [DecidablePred p] (f : (i : ι) → β i) :

↑(Homeomorph.piEquivPiSubtypeProd p β) f = (fun x => f ↑x, fun x => f ↑x)

source

@[simp]

theorem Homeomorph.piEquivPiSubtypeProd_symm_apply {ι : Type u_5} (p : ι → Prop) (β : ι → Type u_6) [(i : ι) → TopologicalSpace (β i)] [DecidablePred p] (f : ((i : { x // p x }) → β ↑i) × ((i : { x // ¬p x }) → β ↑i)) (x : ι) :

↑(Homeomorph.symm (Homeomorph.piEquivPiSubtypeProd p β)) f x = if h : p x then Prod.fst ((i : { x // p x }) → β ↑i) ((i : { x // ¬p x }) → β ↑i) f { val := x, property := h } else Prod.snd ((i : { x // p x }) → β ↑i) ((i : { x // ¬p x }) → β ↑i) f { val := x, property := h }

source

def Homeomorph.piEquivPiSubtypeProd {ι : Type u_5} (p : ι → Prop) (β : ι → Type u_6) [(i : ι) → TopologicalSpace (β i)] [DecidablePred p] :

((i : ι) → β i) ≃ₜ ((i : { x // p x }) → β ↑i) × ((i : { x // ¬p x }) → β ↑i)

The topological space Π i, β i can be split as a product by separating the indices in ι depending on whether they satisfy a predicate p or not.

Instances For

source

@[simp]

theorem Homeomorph.piSplitAt_apply {ι : Type u_5} [DecidableEq ι] (i : ι) (β : ι → Type u_6) [(j : ι) → TopologicalSpace (β j)] (f : (j : ι) → β j) :

↑(Homeomorph.piSplitAt i β) f = (f i, fun j => f ↑j)

source

@[simp]

theorem Homeomorph.piSplitAt_symm_apply {ι : Type u_5} [DecidableEq ι] (i : ι) (β : ι → Type u_6) [(j : ι) → TopologicalSpace (β j)] (f : β i × ((j : { j // j ≠ i }) → β ↑j)) (j : ι) :

↑(Homeomorph.symm (Homeomorph.piSplitAt i β)) f j = if h : j = i then (_ : i = j) ▸ f.fst else Prod.snd (β i) ((j : { j // ¬j = i }) → β ↑j) f { val := j, property := h }

source

def Homeomorph.piSplitAt {ι : Type u_5} [DecidableEq ι] (i : ι) (β : ι → Type u_6) [(j : ι) → TopologicalSpace (β j)] :

((j : ι) → β j) ≃ₜ β i × ((j : { j // j ≠ i }) → β ↑j)

A product of topological spaces can be split as the binary product of one of the spaces and the product of all the remaining spaces.

Instances For

source

@[simp]

theorem Homeomorph.funSplitAt_apply (β : Type u_2) [TopologicalSpace β] {ι : Type u_5} [DecidableEq ι] (i : ι) (f : (j : ι) → (fun a => β) j) :

↑(Homeomorph.funSplitAt β i) f = (f i, fun j => f ↑j)

source

@[simp]

theorem Homeomorph.funSplitAt_symm_apply (β : Type u_2) [TopologicalSpace β] {ι : Type u_5} [DecidableEq ι] (i : ι) (f : (fun a => β) i × ((j : { j // j ≠ i }) → (fun a => β) ↑j)) (j : ι) :

↑(Homeomorph.symm (Homeomorph.funSplitAt β i)) f j = if h : j = i then f.fst else Prod.snd β ({ j // ¬j = i } → β) f { val := j, property := (_ : ¬j = i) }

source

def Homeomorph.funSplitAt (β : Type u_2) [TopologicalSpace β] {ι : Type u_5} [DecidableEq ι] (i : ι) :

(ι → β) ≃ₜ β × ({ j // j ≠ i } → β)

A product of copies of a topological space can be split as the binary product of one copy and the product of all the remaining copies.

Instances For

source

@[simp]

theorem Equiv.toHomeomorph_toEquiv {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ β) (he : ∀ (s : Set β), IsOpen (↑e ⁻¹' s) ↔ IsOpen s) :

(Equiv.toHomeomorph e he).toEquiv = e

source

def Equiv.toHomeomorph {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ β) (he : ∀ (s : Set β), IsOpen (↑e ⁻¹' s) ↔ IsOpen s) :

α ≃ₜ β

An equiv between topological spaces respecting openness is a homeomorphism.

Instances For

source

@[simp]

theorem Equiv.coe_toHomeomorph {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ β) (he : ∀ (s : Set β), IsOpen (↑e ⁻¹' s) ↔ IsOpen s) :

↑(Equiv.toHomeomorph e he) = ↑e

source

theorem Equiv.toHomeomorph_apply {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ β) (he : ∀ (s : Set β), IsOpen (↑e ⁻¹' s) ↔ IsOpen s) (a : α) :

↑(Equiv.toHomeomorph e he) a = ↑e a

source

@[simp]

theorem Equiv.toHomeomorph_refl {α : Type u_5} [TopologicalSpace α] :

Equiv.toHomeomorph (Equiv.refl α) (_ : ∀ (_s : Set α), IsOpen (↑(Equiv.refl α) ⁻¹' _s) ↔ IsOpen (↑(Equiv.refl α) ⁻¹' _s)) = Homeomorph.refl α

source

@[simp]

theorem Equiv.toHomeomorph_symm {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ β) (he : ∀ (s : Set β), IsOpen (↑e ⁻¹' s) ↔ IsOpen s) :

Homeomorph.symm (Equiv.toHomeomorph e he) = Equiv.toHomeomorph e.symm (_ : ∀ (s : Set α), IsOpen (↑e.symm ⁻¹' s) ↔ IsOpen s)

source

theorem Equiv.toHomeomorph_trans {α : Type u_5} {β : Type u_6} {γ : Type u_7} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : α ≃ β) (f : β ≃ γ) (he : ∀ (s : Set β), IsOpen (↑e ⁻¹' s) ↔ IsOpen s) (hf : ∀ (s : Set γ), IsOpen (↑f ⁻¹' s) ↔ IsOpen s) :

Equiv.toHomeomorph (e.trans f) (_ : ∀ (_s : Set γ), IsOpen (↑e ⁻¹' (↑f ⁻¹' _s)) ↔ IsOpen _s) = Homeomorph.trans (Equiv.toHomeomorph e he) (Equiv.toHomeomorph f hf)

source

@[simp]

theorem Equiv.toHomeomorphOfInducing_toEquiv {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ β) (hf : Inducing ↑f) :

(Equiv.toHomeomorphOfInducing f hf).toEquiv = f

source

def Equiv.toHomeomorphOfInducing {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ β) (hf : Inducing ↑f) :

α ≃ₜ β

An inducing equiv between topological spaces is a homeomorphism.

Instances For

source

theorem Continuous.continuous_symm_of_equiv_compact_to_t2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] [T2Space β] {f : α ≃ β} (hf : Continuous ↑f) :

Continuous ↑f.symm

source

@[simp]

theorem Continuous.homeoOfEquivCompactToT2_toEquiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] [T2Space β] {f : α ≃ β} (hf : Continuous ↑f) :

(Continuous.homeoOfEquivCompactToT2 hf).toEquiv = f

source

def Continuous.homeoOfEquivCompactToT2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] [T2Space β] {f : α ≃ β} (hf : Continuous ↑f) :

α ≃ₜ β

Continuous equivalences from a compact space to a T2 space are homeomorphisms.

This is not true when T2 is weakened to T1 (see Continuous.homeoOfEquivCompactToT2.t1_counterexample).

Instances For