exists_lt — Mathlib

English

Let α be a topological space with a preorder and a point a. If 𝓝 a contains points x < a arbitrarily close to a, and p is a property holding for all x in some neighborhood of a, then there exists b < a with p(b).

Русский

Пусть есть точка a в топологическом пространстве с порядком. Если существуют точки меньше a, приближающиеся к a, и если для x близко к a выполняется свойство p, то найдется точка b < a, для которой p(b).

LaTeX

$$${\forall a} \big([\mathrm{NeBot} (𝓝 a) \!, p\big) \Rightarrow \exists b < a, p(b) \big)$$$

Lean4

theorem exists_lt {a : α} [NeBot (𝓝[<] a)] {p : α → Prop} (h : ∀ᶠ x in 𝓝 a, p x) : ∃ b < a, p b :=
  ((frequently_lt_nhds a).and_eventually h).exists

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