inseparableSetoid — Mathlib

English

A setoid on X identifies points that are inseparable; x ~ y iff Inseparable x y; used to form a SeparationQuotient.

Русский

Сетоида на X задаёт эквивалентность x ~ y, если x и y неразделимы; используется для образования SeparationQuotient.

LaTeX

$$$\text{inseparableSetoid}(X)\, :\, \text{Setoid}~X \text{ with } x \sim y \iff 𝓝 x = 𝓝 y$$$

Lean4

/-- A `setoid` version of `Inseparable`, used to define the `SeparationQuotient`. -/
def inseparableSetoid : Setoid X :=
  { Setoid.comap 𝓝 ⊥ with r := Inseparable }

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