Basic lemmas and instances about the WithTopology type synonym

WithTopology X t is a copy of X equipped with the topology t. This is useful for providing multiple topologies on the same type without causing instance conflicts.

In this file we setup basic API about this type and transfer instances (basic, order) from X to WithTopology X t.

Implementation notes

The pattern here is the same one as is used by Lex for order structures and WithLp for metric structures.

theorem WithTopology.ofTopology_toTopology {X : Type u_1} (t : TopologicalSpace X) (x : X) : (toTopology t x).ofTopology = x

@[simp]

theorem WithTopology.toTopology_ofTopology {X : Type u_1} (t : TopologicalSpace X) (x : WithTopology X t) : toTopology t x.ofTopology = x

theorem WithTopology.ofTopology_surjective {X : Type u_1} (t : TopologicalSpace X) : Function.Surjective ofTopology

theorem WithTopology.toTopology_surjective {X : Type u_1} (t : TopologicalSpace X) : Function.Surjective (toTopology t)

theorem WithTopology.ofTopology_injective {X : Type u_1} (t : TopologicalSpace X) : Function.Injective ofTopology

theorem WithTopology.toTopology_injective {X : Type u_1} (t : TopologicalSpace X) : Function.Injective (toTopology t)

theorem WithTopology.ofTopology_bijective {X : Type u_1} (t : TopologicalSpace X) : Function.Bijective ofTopology

theorem WithTopology.toTopology_bijective {X : Type u_1} (t : TopologicalSpace X) : Function.Bijective (toTopology t)

theorem WithTopology.toTopology_inj {X : Type u_1} (t : TopologicalSpace X) {x y : X} : toTopology t x = toTopology t y ↔ x = y

Injectivity lemma for the constructor toTopology t.

It is not marked as @[simp], because its autogenerated version is already in the default simp set.

@[simp]

theorem WithTopology.ofTopology_inj {X : Type u_1} (t : TopologicalSpace X) {x y : WithTopology X t} : x.ofTopology = y.ofTopology ↔ x = y

theorem WithTopology.isOpen_iff {X : Type u_1} (t : TopologicalSpace X) {s : Set (WithTopology X t)} : IsOpen s ↔ IsOpen (toTopology t ⁻¹' s)

theorem WithTopology.isClosed_iff {X : Type u_1} (t : TopologicalSpace X) {s : Set (WithTopology X t)} : IsClosed s ↔ IsClosed (toTopology t ⁻¹' s)

theorem WithTopology.continuous_toTopology {X : Type u_1} (t : TopologicalSpace X) : Continuous (toTopology t)

If X is equipped with topology t, the map X → WithTopology X t is continuous.

theorem WithTopology.continuous_ofTopology {X : Type u_1} (t : TopologicalSpace X) : Continuous ofTopology

If X is equipped with topology t, the map WithTopology X t → X is continuous.

Set-theoretic lemmas

theorem WithTopology.image_ofTopology {X : Type u_1} (t : TopologicalSpace X) (s : Set (WithTopology X t)) : ofTopology '' s = toTopology t ⁻¹' s

theorem WithTopology.preimage_toTopology {X : Type u_1} (t : TopologicalSpace X) (s : Set (WithTopology X t)) : toTopology t ⁻¹' s = ofTopology '' s

theorem WithTopology.image_toTopology {X : Type u_1} (t : TopologicalSpace X) (s : Set X) : toTopology t '' s = ofTopology ⁻¹' s

theorem WithTopology.preimage_ofTopology {X : Type u_1} (t : TopologicalSpace X) (s : Set X) : ofTopology ⁻¹' s = toTopology t '' s

Instance transfers

In this section we transfer some instances from X to WithTopology X t.

instance WithTopology.instNonempty {X : Type u_1} (t : TopologicalSpace X) [Nonempty X] : Nonempty (WithTopology X t)

@[implicit_reducible]

instance WithTopology.instInhabited {X : Type u_1} (t : TopologicalSpace X) [Inhabited X] : Inhabited (WithTopology X t)

Equations

• WithTopology.instInhabited t = { default := WithTopology.toTopology t default }

instance WithTopology.instSubsingleton {X : Type u_1} (t : TopologicalSpace X) [Subsingleton X] : Subsingleton (WithTopology X t)

@[implicit_reducible]

instance WithTopology.instUnique {X : Type u_1} (t : TopologicalSpace X) [Unique X] : Unique (WithTopology X t)

Equations

• WithTopology.instUnique t = Unique.mk' (WithTopology X t)

instance WithTopology.instFinite {X : Type u_1} (t : TopologicalSpace X) [Finite X] : Finite (WithTopology X t)

instance WithTopology.instInfinite {X : Type u_1} (t : TopologicalSpace X) [Infinite X] : Infinite (WithTopology X t)

@[implicit_reducible]

instance WithTopology.instFintype {X : Type u_1} (t : TopologicalSpace X) [Fintype X] : Fintype (WithTopology X t)

Equations

• WithTopology.instFintype t = Fintype.ofBijective (WithTopology.toTopology t) ⋯

def WithTopology.instDecidableEq.decEq {X✝ : Type u_2} {t✝ : TopologicalSpace X✝} [DecidableEq X✝] (x✝ x✝¹ : WithTopology X✝ t✝) : Decidable (x✝ = x✝¹)

Equations

• WithTopology.instDecidableEq.decEq (WithTopology.toTopology t✝ a) (WithTopology.toTopology t✝ b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance WithTopology.instDecidableEq {X✝ : Type u_2} {t✝ : TopologicalSpace X✝} [DecidableEq X✝] : DecidableEq (WithTopology X✝ t✝)

Equations

• WithTopology.instDecidableEq = WithTopology.instDecidableEq.decEq

@[implicit_reducible]

instance WithTopology.instLE {X : Type u_1} (t : TopologicalSpace X) [LE X] : LE (WithTopology X t)

Equations

• WithTopology.instLE t = { le := fun (x y : WithTopology X t) => x.ofTopology ≤ y.ofTopology }

@[implicit_reducible]

instance WithTopology.instLT {X : Type u_1} (t : TopologicalSpace X) [LT X] : LT (WithTopology X t)

Equations

• WithTopology.instLT t = { lt := fun (x y : WithTopology X t) => x.ofTopology < y.ofTopology }

@[implicit_reducible]

instance WithTopology.instDecidableLE {X : Type u_1} (t : TopologicalSpace X) [LE X] [DecidableLE X] : DecidableLE (WithTopology X t)

Equations

• WithTopology.instDecidableLE t x y = inst✝ x.ofTopology y.ofTopology

@[implicit_reducible]

instance WithTopology.instDecidableLT {X : Type u_1} (t : TopologicalSpace X) [LT X] [DecidableLT X] : DecidableLT (WithTopology X t)

Equations

• WithTopology.instDecidableLT t x y = inst✝ x.ofTopology y.ofTopology

@[implicit_reducible]

instance WithTopology.instPreorder {X : Type u_1} (t : TopologicalSpace X) [Preorder X] : Preorder (WithTopology X t)

Equations

• WithTopology.instPreorder t = Preorder.lift WithTopology.ofTopology

@[implicit_reducible]

instance WithTopology.instPartialOrder {X : Type u_1} (t : TopologicalSpace X) [PartialOrder X] : PartialOrder (WithTopology X t)

Equations

• WithTopology.instPartialOrder t = Function.Injective.partialOrder WithTopology.ofTopology ⋯ ⋯ ⋯

@[implicit_reducible]

instance WithTopology.instMax {X : Type u_1} (t : TopologicalSpace X) [Max X] : Max (WithTopology X t)

Equations

• WithTopology.instMax t = { max := fun (x y : WithTopology X t) => WithTopology.toTopology t (x.ofTopology ⊔ y.ofTopology) }

@[implicit_reducible]

instance WithTopology.instMin {X : Type u_1} (t : TopologicalSpace X) [Min X] : Min (WithTopology X t)

Equations

• WithTopology.instMin t = { min := fun (x y : WithTopology X t) => WithTopology.toTopology t (x.ofTopology ⊓ y.ofTopology) }

@[implicit_reducible]

instance WithTopology.instSemilatticeSup {X : Type u_1} (t : TopologicalSpace X) [SemilatticeSup X] : SemilatticeSup (WithTopology X t)

Equations

• WithTopology.instSemilatticeSup t = Function.Injective.semilatticeSup WithTopology.ofTopology ⋯ ⋯ ⋯ ⋯

@[implicit_reducible]

instance WithTopology.instSemilatticeInf {X : Type u_1} (t : TopologicalSpace X) [SemilatticeInf X] : SemilatticeInf (WithTopology X t)

Equations

• WithTopology.instSemilatticeInf t = Function.Injective.semilatticeInf WithTopology.ofTopology ⋯ ⋯ ⋯ ⋯

@[implicit_reducible]

instance WithTopology.instLattice {X : Type u_1} (t : TopologicalSpace X) [Lattice X] : Lattice (WithTopology X t)

Equations

• WithTopology.instLattice t = { toSemilatticeSup := WithTopology.instSemilatticeSup t, inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

@[implicit_reducible]

instance WithTopology.instDistribLattice {X : Type u_1} (t : TopologicalSpace X) [DistribLattice X] : DistribLattice (WithTopology X t)

Equations

• WithTopology.instDistribLattice t = { toLattice := WithTopology.instLattice t, le_sup_inf := ⋯ }

@[implicit_reducible]

instance WithTopology.instOrd {X : Type u_1} (t : TopologicalSpace X) [Ord X] : Ord (WithTopology X t)

Equations

• WithTopology.instOrd t = { compare := fun (x y : WithTopology X t) => compare x.ofTopology y.ofTopology }

@[implicit_reducible]

instance WithTopology.instLinearOrder {X : Type u_1} (t : TopologicalSpace X) [LinearOrder X] : LinearOrder (WithTopology X t)

Equations

• WithTopology.instLinearOrder t = Function.Injective.linearOrder WithTopology.ofTopology ⋯ ⋯ ⋯ ⋯ ⋯ ⋯