Module

Models.lean

Nyll.ValuedFieldTheory.Valuation.Topology.Models

2 declarations indexed from sourceView source ↗

Module documentation

Topological API for `WithTopology`

This file adds only the two topology lemmas used by valuation theory. The underlying type, topology, and basic API come directly from Mathlib. Algebraic structures needed on a particular topology-indexed copy are installed at that copy's owner rather than globally in the root WithTopology namespace.

Imports2

Mathlib.Topology.Homeomorph.Defs
Mathlib.Topology.WithTopology

Imported by5

def

homeomorph

L29 ↗

WithTopology.homeomorph

Documentation

The canonical homeomorphism from Mathlib's topology-indexed copy to its underlying carrier equipped with the indexed topology.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v
namespace WithTopology
variable {X : Type u} {t : TopologicalSpace X}

Lean source · full declaration

def homeomorph {α : Type u} {topology : TopologicalSpace α} :
    @Homeomorph (WithTopology α topology) α
      (inferInstance : TopologicalSpace (WithTopology α topology)) topology where
  toEquiv := WithTopology.equiv α topology
  continuous_toFun := continuous_ofTopology topology
  continuous_invFun := continuous_toTopology topology

theorem

tendsto_nhds_iff

L38 ↗

WithTopology.tendsto_nhds_iff