English
A homomorphism from a uniform group to a discrete uniform group is continuous if and only if its kernel is open.
Русский
Гомоморфизм из униформной группы в дискретную равномерно-типизированную группу непрерывен тогда и только тогда, когда его ядро открыто.
LaTeX
$$$\\text{UniformContinuous}(f) \\iff \\text{IsOpen}(\\ker f)$$$
Lean4
/-- A homomorphism from a uniform group to a discrete uniform group is continuous if and only if
its kernel is open. -/
@[to_additive /-- A homomorphism from a uniform additive group to a discrete uniform additive group
is continuous if and only if its kernel is open. -/
]
theorem uniformContinuous_iff_isOpen_ker {hom : Type*} [UniformSpace β] [DiscreteTopology β] [Group β]
[IsUniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] {f : hom} :
UniformContinuous f ↔ IsOpen ((f : α →* β).ker : Set α) :=
by
refine ⟨fun hf => ?_, fun hf => ?_⟩
· apply (isOpen_discrete ({ 1 } : Set β)).preimage hf.continuous
· apply uniformContinuous_of_continuousAt_one
rw [ContinuousAt, nhds_discrete β, map_one, tendsto_pure]
exact hf.mem_nhds (map_one f)
