topologicalClosure — Mathlib

English

The topological closure of a subfield of a topological field is itself a subfield.

Русский

Топологическое замыкание подполе внутри топологического поля является подполем.

LaTeX

$$TopologicalClosure(K) is a Subfield$$

Lean4

/-- The (topological-space) closure of a subfield of a topological field is
itself a subfield. -/
def topologicalClosure (K : Subfield α) : Subfield α :=
  { K.toSubring.topologicalClosure with
    carrier := _root_.closure (K : Set α)
    inv_mem' := fun x hx => by
      rcases eq_or_ne x 0 with (rfl | h)
      · rwa [inv_zero]
      · rw [← inv_coe_set, ← Set.image_inv_eq_inv]
        exact mem_closure_image (continuousAt_inv₀ h) hx }

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