English
Given i: α→β dense inducing and f: α→γ, one can define an extension di.extend f : β→γ extending f along i; under favorable conditions this extension is unique.
Русский
Дано плотное индуциирующее отображение i: α→β и функция f: α→γ. Тогда существует продолжение di.extend f : β→γ, расширяющее f по i; при благоприятных условиях оно является уникальным.
LaTeX
$$$\\text{extend }(\\text{di})(f) : β \\to γ$$$
Lean4
/-- If `i : α → β` is a dense inducing, then any function `f : α → γ` "extends" to a function `g =
IsDenseInducing.extend di f : β → γ`. If `γ` is Hausdorff and `f` has a continuous extension, then
`g` is the unique such extension. In general, `g` might not be continuous or even extend `f`. -/
def extend (di : IsDenseInducing i) (f : α → γ) (b : β) : γ :=
@limUnder _ _ _ ⟨f (di.dense.some b)⟩ (comap i (𝓝 b)) f
