productOfMemOpens_injective — Mathlib

English

If X is a T0 space, then the map x ↦ (x ∈ U) is injective, i.e., distinct points are distinguished by opens.

Русский

Если X — пространство T0, то отображение x ↦ (x ∈ U) инъективно, то есть различные точки различаются открытыми множелствами.

LaTeX

$$$\text{If } [T_0(X)],\; \text{Injective}(\text{productOfMemOpens } X).$$$

Lean4

theorem productOfMemOpens_injective [T0Space X] : Function.Injective (productOfMemOpens X) :=
  by
  intro x1 x2 h
  apply Inseparable.eq
  rw [← IsInducing.inseparable_iff (productOfMemOpens_isInducing X), h]

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