eq

Mathlib.Order.InitialSeg

URI: https://scilib.ai/kg/mathlib#InitialSeg.eq

English

If f is an InitialSeg embedding and g is a RelIso, then for any a, g a = f a.

Русский

Если f — вложение InitialSeg, а g — RelIso, то для любого a выполняется g a = f a.

LaTeX

$$$[IsWellOrder \\ β \\ s] (f : r ≼i s) (g : r \\simeq_r s) (a : α) : g a = f a.$$$

Lean4

protected theorem eq [IsWellOrder β s] (f g : r ≼i s) (a) : f a = g a := by rw [Subsingleton.elim f g]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru