English
The product of two dense embeddings e1 and e2 is a dense embedding of the product spaces, given by p ↦ (e1 p1, e2 p2).
Русский
Произведение двух плотных вложений является плотным вложением на произведении пространств, через отображение p ↦ (e1 p1, e2 p2).
LaTeX
$$$IsDenseEmbedding (fun p: \\alpha \\times \\gamma \\Rightarrow (e_1 p.1, e_2 p.2))$$$
Lean4
/-- This is a shortcut for `hs.isDenseInducing_val.extend f`. It is useful because if `s : Set α`
is dense then the coercion `(↑) : s → α` automatically satisfies `IsUniformInducing` and
`IsDenseInducing` so this gives access to the theorems satisfied by a uniform extension by simply
mentioning the density hypothesis. -/
noncomputable def extend (hs : Dense s) (f : s → β) : α → β :=
hs.isDenseInducing_val.extend f
