not_forall₂_of_exists₂_not

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#not_forall₂_of_exists₂_not

English

If there exists a counterexample to P x h, then not all x,h satisfy P x h.

Русский

Если существует контрпример к P x h, то не выполнено утверждение ∀ x,h, P x h.

LaTeX

$$$\bigl(\exists x,h\, \lnot P(x,h)\bigr) \to \lnot\forall x,h\, P(x,h).$$$

Lean4

theorem not_forall₂_of_exists₂_not : (∃ x h, ¬P x h) → ¬∀ x h, P x h
  | ⟨x, h, hp⟩, al => hp <| al x h

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

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

Разделы

Аффилиация

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