forall_ne_bot — Mathlib

English

For any predicate p on WithBot α, (∀ x, x ≠ ⊥ → p x) holds iff ∀ a ∈ α, p (withBot a).

Русский

Для любого предиката p на WithBot α выполняется (∀ x, x ≠ ⊥ → p x) тогда и только тогда, что ∀ a ∈ α, p (withBot a).

LaTeX

$$$(\forall x, x \neq ⊥ \rightarrow p x) \iff \forall a : α, p (\mathrm{some}\ a)$$$

Lean4

theorem forall_ne_bot {p : WithBot α → Prop} : (∀ x, x ≠ ⊥ → p x) ↔ ∀ x : α, p x := by simp [ne_bot_iff_exists]

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