isSuccPrelimit_apply_iff

Mathlib.Order.SuccPred.InitialSeg

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

English

For an embedding f: α ↪ β, IsSuccPrelimit (f a) is equivalent to IsSuccPrelimit a.

Русский

Для вложения f: α → β равносильно IsSuccPrelimit (f a) и IsSuccPrelimit a.

LaTeX

$$$IsSuccPrelimit(f(a)) \iff IsSuccPrelimit(a)$$$

Lean4

@[simp]
theorem isSuccPrelimit_apply_iff (f : α <i β) : IsSuccPrelimit (f a) ↔ IsSuccPrelimit a :=
  (f : α ≤i β).isSuccPrelimit_apply_iff

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

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

Разделы

Аффилиация

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