isSuccLimit_apply_iff

Mathlib.Order.SuccPred.InitialSeg

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

English

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

Русский

Для вложения f: α → β IsSuccLimit (f a) ⇔ IsSuccLimit a.

LaTeX

$$$IsSuccLimit(f(a)) \iff IsSuccLimit(a)$$$

Lean4

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

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

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

Разделы

Аффилиация

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