ClosureSpace.FiniteHomeomorph
structure
Packages one bijection together with finite continuity of the map and its actual inverse.
Statement
Let and be closure spaces. A finite-homeomorphism from to is a bijection whose forward map and actual inverse both preserve closure on finite test subsets. It is a structure carrying the map and these two properties, rather than only a proposition asserting that some map exists.
Definition
For a function and a subset of its domain, write . A finite-homeomorphism consists of a bijection , with its inverse , satisfying
and
The inverse in the second inclusion belongs to the same bijection: and . The first inclusion transports every point of the closure of a finite source set into the closure of its image. The second imposes the corresponding requirement in the reverse direction.
Here “finite” qualifies the test sets and . The sets , the image , and the closures need not be finite. The closure operations themselves still act on all subsets.
Assumptions
The two given closure operations are extensive, monotone and idempotent and preserve the empty set. The carriers may be empty and may belong to independent universes. No topology, metric, dimension bound or finite-character property of either closure is an input.
Full continuity would require the first inclusion for every subset of , not only finite ones, and similarly for the inverse on . Neither full-continuity requirement is a field of this structure.
Conclusion
An element of the defined type supplies one invertible map with both finite-continuity properties. These data can be used wherever a finite-homeomorphism is required without supplying ordinary continuity.
The separately defined continuous finite-homeomorphism adds full continuity of the forward map; even that additional structure does not include inverse full continuity. This distinction concerns an extra field, not a change to the underlying closure operators.
Main citations
- Finite-homeomorphism: the complete structure, lines 157–159: the equivalence and its two finite-continuity fields.
- Full and finite continuity, lines 29–34: the arbitrary-set and finite-set tests.
- The additional forward full-continuity field, lines 163–165:
ContinuousFiniteHomeomorph. - Closure spaces before topology, for the underlying closure axioms; fixed source, lines 28–30 and 37–61.
Lean source signature (exact)
Exact declaration. The complete structure, including its parent and both fields is shown below.
structure FiniteHomeomorph (c : ClosureSpace α) (d : ClosureSpace β) extends α ≃ β where
finitelyContinuous_toFun : c.FinitelyContinuous d toFun
finitelyContinuous_invFun : d.FinitelyContinuous c invFun
| In the source | Mathematical meaning |
|---|---|
Exact declaration{α : Type u}, {β : Type v} in the surrounding scope |
The arbitrary carriers , in independent universes. The nearby third carrier is unused by this declaration. |
Exact declaration(c : ClosureSpace α) (d : ClosureSpace β) |
The given closure operations on all subsets of the two carriers. |
Exact declarationextends α ≃ β |
Data of one bijection and its actual inverse, including the inverse identities. |
Exact declarationfinitelyContinuous_toFun : c.FinitelyContinuous d toFun |
For every finite , . |
Exact declarationfinitelyContinuous_invFun : d.FinitelyContinuous c invFun |
For every finite , the inverse of that same satisfies . |
Exact declaration∀ s : Set α, s.Finite → ... in the separate predicate excerpt |
Finiteness belongs to the tested subset, not to the carrier or all values of the map. |
Exact declarationf '' s in the continuity predicates |
The image of a set is written in the exposition. |
Exact declarationFiniteHomeomorph c d |
A type of maps with specified properties; its definition does not assert that this type is inhabited. |
Exact surrounding scope and supporting definitions
The following source excerpts are separate from the declaration above. Their line ranges are not concatenated into a synthetic signature.
Source Maps.lean, lines 22–26:
universe u v w
namespace ClosureSpace
variable {α : Type u} {β : Type v} {γ : Type w}
Source Maps.lean, lines 29–34:
def Continuous (c : ClosureSpace α) (d : ClosureSpace β) (f : α → β) : Prop :=
∀ s : Set α, f '' c.closure s ⊆ d.closure (f '' s)
/-- Preservation of closure, tested only on finite subsets of the domain. -/
def FinitelyContinuous (c : ClosureSpace α) (d : ClosureSpace β) (f : α → β) : Prop :=
∀ s : Set α, s.Finite → f '' c.closure s ⊆ d.closure (f '' s)
Source Maps.lean, lines 163–165:
structure ContinuousFiniteHomeomorph (c : ClosureSpace α) (d : ClosureSpace β)
extends FiniteHomeomorph c d where
continuous_toFun : c.Continuous d toFun
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project