forall — Mathlib

English

A property holds for every interval if and only if it holds at the bottom and for every nonempty interval.

Русский

Свойство выполняется для каждого интервала тогда и только тогда, когда оно выполняется в нижнем интервале и для каждого непустого интервала.

LaTeX

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

Lean4

protected theorem «forall» {p : Interval α → Prop} : (∀ s, p s) ↔ p ⊥ ∧ ∀ s : NonemptyInterval α, p s :=
  Option.forall

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