not_forall₂ — Mathlib

English

Under decidability hypotheses, (not for all) is equivalent to the existence of a counterexample.

Русский

При допущении разрешимости не для всех эквивалентно существованию контрпримерa.

LaTeX

$$$\text{[Decidable]}\;\bigl(\lnot \forall x,h\, P(x,h)\bigr) \iff \exists x,h\, \lnot P(x,h).$$$

Lean4

protected theorem not_forall₂ [Decidable (∃ x h, ¬P x h)] [∀ x h, Decidable (P x h)] :
    (¬∀ x h, P x h) ↔ ∃ x h, ¬P x h :=
  ⟨Not.decidable_imp_symm fun nx x h ↦ nx.decidable_imp_symm fun h' ↦ ⟨x, h, h'⟩, not_forall₂_of_exists₂_not⟩

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