uniformly_extend_unique — Mathlib

English

Given h := IsUniformInducing e and dense, the extension is unique: any g extending f equals ψ.

Русский

Для данных e и плотного образа продолжение единственно: любая g, которая расширяет f, равна ψ.

LaTeX

$$$\text{If } g:\alpha\to\gamma,\; g\text{ extends } f, \text{ then } g=\psi.$$$

Lean4

theorem uniformly_extend_unique {g : α → γ} (hg : ∀ b, g (e b) = f b) (hc : Continuous g) : ψ = g :=
  IsDenseInducing.extend_unique _ hg hc

Похожие утверждения