preorder — Mathlib

English

The space of finitely supported functions ι →₀ M carries a natural preorder defined pointwise, making it a preordered set.

Русский

Множество конечно поддерживаемых функций ι →₀ M снабжено естественным порядком, определяемым по каждой точке, образуя предпорядок.

LaTeX

$$$\text{Preorder}(ι \to₀ M).$$$

Lean4

instance preorder : Preorder (ι →₀ M) where
  le_refl _ _ := le_rfl
  le_trans _ _ _ hfg hgh i := (hfg i).trans (hgh i)

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