bijective — Mathlib

English

If h: α ≃ᵤ β is a uniform equivalence, then its underlying function is bijective.

Русский

Если h: α ≃ᵤ β — равномерное эквивалентность, тогда соответствующее отображение является биекцией.

LaTeX

$$$\\forall {\\alpha \\beta} [UniformSpace \\alpha] [UniformSpace \\beta] (h : \\alpha \\simeq_u \\beta),\\; Bijective(h)$$$

Lean4

protected theorem bijective (h : α ≃ᵤ β) : Function.Bijective h :=
  h.toEquiv.bijective

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