isEmbedding_val₀ — Mathlib

English

If the inversion is continuous at all nonzero points, then the natural inclusion of the unit group G₀ˣ into G₀ is a topological embedding.

Русский

Если обращение непрерывно во всех ненулевых точках, тогда внедрение группы единиц G₀ˣ в G₀ является топологическим вложением.

LaTeX

$$$\\text{IsEmbedding}(\\mathrm{val} : G_0^{\\times} \\to G_0)$$$

Lean4

/-- If `G₀` is a group with zero with topology such that `x ↦ x⁻¹` is continuous at all nonzero
points. Then the coercion `G₀ˣ → G₀` is a topological embedding. -/
theorem isEmbedding_val₀ : IsEmbedding (val : G₀ˣ → G₀) :=
  embedding_val_mk <| (continuousOn_inv₀ (G₀ := G₀)).mono fun _ ↦ IsUnit.ne_zero

Похожие утверждения