completableTopField — Mathlib

English

If a field L is complete, its uniform structure yields a completable topological field structure on L.

Русский

Если кольцо L полно, то с его униформной структурой L становится полноценно-совмещаемой топологической полем.

LaTeX

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

Lean4

instance completableTopField (K : Subfield L) : CompletableTopField K where
  nice F F_cau
    inf_F := by
    let i : K →+* L := K.subtype
    have hi : IsUniformInducing i := isUniformEmbedding_subtype_val.isUniformInducing
    rw [← hi.cauchy_map_iff] at F_cau ⊢
    rw [map_comm (show (i ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ i by ext; rfl)]
    apply CompletableTopField.nice _ F_cau
    rw [← Filter.push_pull', ← map_zero i, ← hi.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]

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