orderIsoOfSurjective_symm_apply_self

Mathlib.Order.Hom.Set

URI: https://scilib.ai/kg/mathlib#StrictMono.orderIsoOfSurjective_symm_apply_self

← MathLib Explorer

English

For all a in α, (orderIsoOfSurjective f h_mono h_surj).symm (f a) = a, i.e. inverse maps back.

Русский

Для любого a выполняется (orderIsoOfSurjective(...)).symm (f a) = a.

LaTeX

$$$(orderIsoOfSurjective\, f\, h_mono\, h_surj).symm (f\, a) = a$$$

Lean4

@[simp]
theorem orderIsoOfSurjective_symm_apply_self (a : α) : (orderIsoOfSurjective f h_mono h_surj).symm (f a) = a :=
  (orderIsoOfSurjective f h_mono h_surj).symm_apply_apply _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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