exists_gt — Mathlib

English

Let α be a preorder with a topology. If nhds[a] restricted to points greater than a is nonempty and p holds eventually near a, then there exists b > a with p(b).

Русский

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

LaTeX

$$$\\forall a, (\\mathcal{N}_{>}(a).NeBot) \\Rightarrow (\\forall p, (\\forall^\\infty x \\in 𝓝 a, p x) \\Rightarrow \\exists b > a, p(b))$$$

Lean4

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

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