forall_ne_top — Mathlib

English

Let p be a predicate on WithTop(α). Then (for all x, x ≠ ⊤ → p(x)) holds if and only if (for all a ∈ α, p(↑a)).

Русский

Пусть p — предикат на WithTop(α). Тогда (∀x, x ≠ ⊤ → p(x)) эквивалентно (∀a ∈ α, p(↑a)).

LaTeX

$$$(\forall x : \mathrm{WithTop}(\alpha),\ x \neq \top \rightarrow p(x)) \iff (\forall a : \alpha,\ p(\uparrow a))$$$

Lean4

theorem forall_ne_top {p : WithTop α → Prop} : (∀ x, x ≠ ⊤ → p x) ↔ ∀ x : α, p x := by simp [ne_top_iff_exists]

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