English
If Nat.cast has dense range and κ1, κ2 are continuous AddChar with κ1(1)=κ2(1), then κ1=κ2.
Русский
Если Nat.cast имеет плотное покрытие, и κ1, κ2 — непрерывные AddChar, причем κ1(1)=κ2(1), то κ1=κ2.
LaTeX
$$$\\text{DenseRange Nat.cast} \\Rightarrow \\forall {κ_1 κ_2 : AddChar A M},\\;\\text{Continuous}(κ_1) \\to \\text{Continuous}(κ_2) \\to (κ_1 1 = κ_2 1) \\to κ_1 = κ_2$$$
Lean4
theorem continuous_map (M : Type*) [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {X Y : Type*} [Finite X]
[Finite Y] (f : X → Y) : Continuous (FunOnFinite.map (M := M) f) := by
classical
have := Fintype.ofFinite X
refine continuous_pi (fun y ↦ ?_)
simp only [FunOnFinite.map_apply_apply]
exact continuous_finset_sum _ (fun _ _ ↦ continuous_apply _)
