Mathlib Map

Theorems · Theorem · complex analysis

RCLike.isUniformEmbedding_ofReal

∀ {𝕜 : Type u_2} [inst : RCLike 𝕜], IsUniformEmbedding RCLike.ofReal
Defined in
Mathlib.Analysis.Complex.Basic
Cited by
1 results in Mathlib
Foundations
Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
RCLike
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Filter.tendsto_ofReal_iff' · cited by 1Filter.tendsto_ofReal_iff'Real · cited by 25697RealRCLike · cited by 2829RCLikeRCLike.ofReal · cited by 350RCLike.ofRealIsUniformEmbedding · cited by 107IsUniformEmbeddingLinearIsometry.isometry · cited by 24LinearIsometry.isometryRCLike.ofRealLI · cited by 6RCLike.ofRealLIIsometry.isUniformEmbedding · cited by 4Isometry.isUniformEmbeddi…RCLike.isUniformEmbedding_ofR…CITED BYCITES

Cites7

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

Cited by1

Results whose statement or proof uses this declaration.