completableTopField_of_complete — Mathlib

English

A complete field with a compatible uniform structure admits a completable top field structure.

Русский

Полное поле с совместной униформной структурой допускает структуру completableTopField.

LaTeX

$$$\text{CompletableTopField}(L)$$$

Lean4

instance (priority := 100) completableTopField_of_complete (L : Type*) [Field L] [UniformSpace L]
    [IsTopologicalDivisionRing L] [T0Space L] [CompleteSpace L] : CompletableTopField L where
  nice F cau_F
    hF := by
    haveI : NeBot F := cau_F.1
    rcases CompleteSpace.complete cau_F with ⟨x, hx⟩
    have hx' : x ≠ 0 := by
      rintro rfl
      rw [inf_eq_right.mpr hx] at hF
      exact cau_F.1.ne hF
    exact
      Filter.Tendsto.cauchy_map <|
        calc
          map (fun x => x⁻¹) F ≤ map (fun x => x⁻¹) (𝓝 x) := map_mono hx
          _ ≤ 𝓝 x⁻¹ := continuousAt_inv₀ hx'

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