instPreorder — Mathlib

English

The collection of partial isomorphisms from α to β carries a natural preorder, defined by comparing the underlying maps of two partial isomorphisms.

Русский

Множество частичных изоморфизмов из α в β обладает естественным предпорядком, определяемым сравнением соответствующих отображений двух частичных изоморфизмов.

LaTeX

$$$\\\\forall f,g \\\\in \\\\mathrm{PartialIso}(\\\\alpha,\\\\beta),\\\\ f \\\\\\le g \\\\iff f.\\\\mathrm{val} \\\\le g.\\\\mathrm{val}. $$$

Lean4

instance : Preorder (PartialIso α β) :=
  Subtype.preorder _

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