not_ex_isAtomic — Mathlib

English

For any φ ∈ L.BoundedFormula α (n + 1), the existentially quantified φ.ex is not atomic.

Русский

Для любой φ ∈ L.BoundedFormula α (n+1) существование по φ.ex не является атомарной формулой.

LaTeX

$$$\forall {L} {\alpha} {n} (\varphi : L.BoundedFormula \alpha (n + 1)), \neg ((\varphi.ex).IsAtomic).$$$

Lean4

theorem not_ex_isAtomic (φ : L.BoundedFormula α (n + 1)) : ¬φ.ex.IsAtomic := fun con => by cases con

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