injective — Mathlib

English

If a map f is topology-inducing and the domain is a T0 space, then f is injective.

Русский

Если отображение f индуктивно задает топологию на образе и область является T0-пространством, то f инъективно.

LaTeX

$$$\text{If } hf : \text{IsInducing}(f) \text{ and } [T0Space(X)], \text{ then } Injective(f).$$$

Lean4

/-- A topology inducing map from a T₀ space is injective. -/
protected theorem injective [TopologicalSpace Y] [T0Space X] {f : X → Y} (hf : IsInducing f) : Injective f :=
  fun _ _ h => (hf.inseparable_iff.1 <| .of_eq h).eq

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