subrelIso_apply

Mathlib.Order.InitialSeg

URI: https://scilib.ai/kg/mathlib#PrincipalSeg.subrelIso_apply

English

For any a, f.subrelIso(⟨f(a), f.lt_top(a)⟩) = a.

Русский

Для любого a выполняется f.subrelIso(⟨f(a), f.lt_top(a)⟩) = a.

LaTeX

$$$f.\\mathrm{subrelIso}(\\langle f(a), f.lt\\_top(a)\\rangle) = a$$$

Lean4

@[simp]
theorem subrelIso_apply (f : r ≺i s) (a : α) : f.subrelIso ⟨f a, f.lt_top a⟩ = a :=
  Equiv.ofInjective_symm_apply f.injective _

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

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

Разделы

Аффилиация

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