exists — Mathlib

English

There exists an interval with property p if and only if either the bottom has p or some nonempty interval has p.

Русский

Существует интервал с свойством p тогда и только тогда, когда либо нижний имеет p, либо какой-то непустой интервал имеет p.

LaTeX

$$$ (\exists s: \mathrm{Interval}(\alpha), p(s)) \iff p(\bot) \lor \exists s: \mathrm{NonemptyInterval}(\alpha), p(s) $$$

Lean4

protected theorem «exists» {p : Interval α → Prop} : (∃ s, p s) ↔ p ⊥ ∨ ∃ s : NonemptyInterval α, p s :=
  Option.exists

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