Mathlib Map

Theorems · Theorem · field theory

CompletableTopField.nice

∀ {K : Type u_1} {inst : Field K} {inst_1 : UniformSpace K} [self : CompletableTopField K] (F : Filter K),
  Cauchy F → nhds 0 ⊓ F = ⊥ → Cauchy (Filter.map (fun x => x⁻¹) F)
Defined in
Mathlib.Topology.Algebra.UniformField
Cited by
2 results in Mathlib
Foundations
Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CompletableTopField
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

UniformSpace.Completion.continuous_hatInv · cited by 1Completion.continuous_hat…IsUniformInducing.completableTopField · cited by 0IsUniformInducing.complet…Filter · cited by 8121FilterField · cited by 7404Fieldnhds · cited by 5554nhdsBot.bot · cited by 4720Bot.botUniformSpace · cited by 2040UniformSpaceFilter.map · cited by 819Filter.mapCauchy · cited by 115CauchyCompletableTopField · cited by 5CompletableTopFieldCompletableTopField.niceCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.