isSuccPrelimit_apply_iff — Mathlib

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

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