and_forall_ne — Mathlib

English

Assume α has decidable equality. Then for any a in α, (p(a) ∧ ∀ b, b ≠ a → p(b)) is equivalent to ∀ b, p(b).

Русский

Пусть имеется разрешимое равенство на α. Тогда для любого a: (p(a) ∧ ∀ b, b ≠ a → p(b)) эквивалентно ∀ b, p(b).

LaTeX

$$$$(p(a) \\land \\forall b, b \\neq a \\to p(b)) \\leftrightarrow \\forall b, p(b).$$$$

Lean4

theorem and_forall_ne [DecidableEq α] (a : α) {p : α → Prop} : (p a ∧ ∀ b, b ≠ a → p b) ↔ ∀ b, p b := by
  simp only [← @forall_eq _ p a, ← forall_and, ← or_imp, Decidable.em, forall_const]

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