English
Let f be a map between ordered sets that preserves the initial-segment structure. Then for every a, the property IsSuccPrelimit is preserved under f, i.e., IsSuccPrelimit (f a) ⇔ IsSuccPrelimit a.
Русский
Пусть f — отображение между упорядоченными множествами, сохраняющее структуру начального отрезка. Тогда для любого a выполнено: 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 :=
by
constructor <;> intro h b hb
· rw [← f.apply_covBy_apply_iff] at hb
exact h _ hb
· obtain ⟨c, rfl⟩ := f.mem_range_of_rel hb.lt
rw [f.apply_covBy_apply_iff] at hb
exact h _ hb