Theorems · Definition · field theory

CompletableTopField.recOn

{K : Type u_1} →
  [inst : Field K] →
    [inst_1 : UniformSpace K] →
      {motive : CompletableTopField K → Sort u} →
        (t : CompletableTopField K) →
          ([toT0Space : T0Space K] →
              (nice : ∀ (F : Filter K), Cauchy F → nhds 0 ⊓ F = ⊥ → Cauchy (Filter.map (fun x => x⁻¹) F)) → motive ⋯) →
            motive t

Defined in

Mathlib.Topology.Algebra.UniformField

Cited by

0 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldUniformSpace