and_forall_ne

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#and_forall_ne

English

For any a, (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) \\wedge \\forall b, b \\neq a \\to p(b)) \\leftrightarrow \\forall b, p(b).$$$$

Lean4

theorem and_forall_ne (a : α) : (p a ∧ ∀ b, b ≠ a → p b) ↔ ∀ b, p b :=
  open scoped Classical in Decidable.and_forall_ne a

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru