Commit 2024-09-29 00:04 0668f239

View on Github →

chore: Rename DenseInducing to IsDenseInducing (#17208) 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 DenseInducing is)
  2. namespacing it inside Topology Zulip. See #15993 for context.

Estimated changes

deleted theorem DenseInducing.dense_image
deleted theorem DenseInducing.extend_eq'
deleted theorem DenseInducing.extend_eq
deleted theorem DenseInducing.mk'
deleted structure DenseInducing
added theorem IsDenseInducing.mk'
added structure IsDenseInducing