inter_Ioo_nonempty — Mathlib

English

If o is an accumulation point of S, then for every p < o, the intersection S ∩ (p,o) is nonempty.

Русский

Если o — точка накопления S, то для каждого p < o множество S ∩ (p,o) непусто.

LaTeX

$$inter_Ioo_nonempty {o : Ordinal} {S : Set Ordinal} (hS : o.IsAcc S) {p : Ordinal} (hp : p < o) : (S ∩ Ioo p o).Nonempty$$

Lean4

theorem inter_Ioo_nonempty {o : Ordinal} {S : Set Ordinal} (hS : o.IsAcc S) {p : Ordinal} (hp : p < o) :
    (S ∩ Ioo p o).Nonempty :=
  hS.forall_lt p hp

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