English
Let h be an L-extension pair between structures N and M. For a fixed element n in N, the collection of finitely generated L-equivalences f between M and N whose codomain contains n forms a cofinal subset of the directed order of all such equivalences.
Русский
Пусть h является парой расширения на языке L между структурами N и M. Для заданного элемента n ∈ N множество всех конечных эквивалентностей f между M и N, удовлетворяющих условию n ∈ cod(f), образует кофинальное подмножество частичных эквивалентностей между M и N в направлении включения.
LaTeX
$$$S := \\{ f \\in FGEquiv_L M N \\mid n \\in cod(f) \\}, \\quad S \\text{ кофинально в } FGEquiv_L M N \\text{ относительно } \\le,$$$
Lean4
/-- The cofinal set of finite equivalences with a given element in their codomain. -/
def definedAtRight (h : L.IsExtensionPair N M) (n : N) : Order.Cofinal (FGEquiv L M N)
where
carrier := {f | n ∈ f.val.cod}
isCofinal := fun f => h.cod f n
