map_isSuccLimit — Mathlib

English

Another form of le_iff_forall_le for IsNormal f relates upper bounds via isLUB.

Русский

Ещё одна форма равносвязи неравенства IsNormal через isLUB.

LaTeX

$$$\text{IsNormal}(f) \to (\text{IsLUB} \; \text{??})$$$

Lean4

theorem map_isSuccLimit (hf : IsNormal f) (ha : IsSuccLimit a) : IsSuccLimit (f a) :=
  by
  refine ⟨?_, fun b hb ↦ ?_⟩
  · obtain ⟨b, hb⟩ := not_isMin_iff.1 ha.not_isMin
    exact not_isMin_iff.2 ⟨_, hf.strictMono hb⟩
  · obtain ⟨c, hc, hc'⟩ := (hf.lt_iff_exists_lt ha).1 hb.lt
    have hc' := hb.ge_of_gt hc'
    rw [hf.strictMono.le_iff_le] at hc'
    exact hc.not_ge hc'

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