Commit 2024-10-08 15:03 fa055566

View on Github →

chore: Rename UniformInducing to IsUniformInducing (#17398) Function.Embedding is a type while Embedding is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards

  1. renaming Embedding to IsEmbedding and similarly for neighborhing declarations (which UniformInducing is)
  2. namespacing it inside Topology Zulip. See #15993 for context.

Estimated changes

modified structure IsUniformEmbedding
added theorem IsUniformInducing.comp
added theorem IsUniformInducing.id
added theorem IsUniformInducing.mk'
added theorem IsUniformInducing.prod
added structure IsUniformInducing
deleted theorem UniformInducing.comp
deleted theorem UniformInducing.inducing
deleted theorem UniformInducing.mk'
deleted theorem UniformInducing.prod
deleted structure UniformInducing
modified theorem completeSpace_extension
modified theorem isComplete_image_iff
added theorem isUniformInducing_iff'
modified theorem totallyBounded_image_iff
modified theorem totallyBounded_preimage
deleted theorem uniformInducing_id
deleted theorem uniformInducing_iff'