trans — Mathlib

English

Specialization is transitive: if x specializes to y and y specializes to z, then x specializes to z.

Русский

Специализация является транзитивной: если x специализируется на y, а y — на z, то x специализируется на z.

LaTeX

$$$$\forall X\ [\text{TopologicalSpace } X],\ \forall x,y,z:X,\ (x \rightsquigarrow y)\land (y \rightsquigarrow z)\ \Rightarrow\ (x \rightsquigarrow z).$$$$

Lean4

@[trans]
theorem trans : x ⤳ y → y ⤳ z → x ⤳ z :=
  le_trans

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