specializes_iff_pure — Mathlib

English

x specializes to y if and only if the pure filter at x is less than or equal to the neighborhood filter at y.

Русский

x специализируется на y тогда и только тогда, когда чистый фильтр на x меньше или равен фильтру окрестностей y.

LaTeX

$$$ x \;⤳\; y \iff \mathrm{pure}(x) \le \mathcal{N}(y)$$$

Lean4

theorem specializes_iff_pure : x ⤳ y ↔ pure x ≤ 𝓝 y :=
  (specializes_TFAE x y).out 0 1

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