isSuccLimit_of_mem_frontier — Mathlib

English

If a is in the frontier of s, then a is a succ-limit ordinal.

Русский

Если a ∈ frontier s, то a является succ-пределом.

LaTeX

$$Forall ha: a ∈ frontier s, IsSuccLimit a$$

Lean4

theorem isSuccLimit_of_mem_frontier (ha : a ∈ frontier s) : IsSuccLimit a :=
  by
  simp only [frontier_eq_closure_inter_closure, Set.mem_inter_iff, mem_closure_iff] at ha
  by_contra h
  rw [← isOpen_singleton_iff] at h
  rcases ha.1 _ h rfl with ⟨b, hb, hb'⟩
  rcases ha.2 _ h rfl with ⟨c, hc, hc'⟩
  rw [Set.mem_singleton_iff] at *
  subst hb; subst hc
  exact hc' hb'

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