exists_ne_top — Mathlib

English

There exists an x ∈ WithTop(α) with x ≠ ⊤ and p(x) if and only if there exists a ∈ α with p(↑a).

Русский

Существует x ∈ WithTop(α) такое, что x ≠ ⊤ и p(x) тогда и только тогда, когда существует a ∈ α, такое что p(↑a).

LaTeX

$$$(\exists x \neq \top,\ p(x)) \iff (\exists x : \alpha,\ p(\uparrow x))$$$

Lean4

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

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