Embedding.inj
theorem Embedding.inj :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
Embedding f → Function.Injective f
The theorem states that for any two types `X` and `Y`, given that they are both topological spaces, any function `f` that maps `X` to `Y` and qualifies as a topological embedding is necessarily injective. In other words, if `f` is a topological embedding from `X` to `Y`, then for any two elements `a₁` and `a₂` in `X`, if `f(a₁)` equals `f(a₂)`, it must be the case that `a₁` equals `a₂`.
More concisely: If `X` and `Y` are topological spaces and `f : X → Y` is a topological embedding, then `f` is injective.
|
Inducing.induced
theorem Inducing.induced :
∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
Inducing f → tX = TopologicalSpace.induced f tY
The theorem states that for any types `X` and `Y` equipped with topological spaces `tX` and `tY` respectively, and for any function `f` from `X` to `Y`, if `f` is an inducing function, then the topology on `X` (`tX`) equals the topology on `X` induced by `f` from the topology on `Y` (`tY`). This essentially means that the topology of the domain `X` under the function `f` is precisely the coarsest topology that makes `f` continuous.
More concisely: If `f` is an inducing function from topological spaces `tX` on `X` to `tY` on `Y`, then `tX` equals the induced topology on `X` from `tY` through `f`.
|