orderIsoOfSurjective_self_symm_apply

Mathlib.Order.Hom.Set

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

← MathLib Explorer

English

For any b in β, f((orderIsoOfSurjective f h_mono h_surj).symm b) = b; the forward map undoes the inverse.

Русский

Для любого b верно f((orderIsoOfSurjective(...)).symm b) = b.

LaTeX

$$$f\bigl((orderIsoOfSurjective\, f\, h_mono\, h_surj).symm\, b\bigr) = b$$$

Lean4

theorem orderIsoOfSurjective_self_symm_apply (b : β) : f ((orderIsoOfSurjective f h_mono h_surj).symm b) = b :=
  (orderIsoOfSurjective f h_mono h_surj).apply_symm_apply _

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

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

Разделы

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

Аффилиация

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