not_mem_iff — Mathlib

English

For any p and φ, φ.not ∈ p iff φ ∉ p.

Русский

Для любого p и φ, φ.not ∈ p тогда и только тогда φ ∉ p.

LaTeX

$$$\\\\phi.not \\\\in p \\\\iff \\\\phi \\notin p$$$

Lean4

theorem not_mem_iff (p : T.CompleteType α) (φ : L[[α]].Sentence) : φ.not ∈ p ↔ φ ∉ p :=
  ⟨fun hf ht =>
    by
    have h : ¬IsSatisfiable ({ φ, φ.not } : L[[α]].Theory) :=
      by
      rintro ⟨@⟨_, _, h, _⟩⟩
      simp only [model_iff, mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq] at h
      exact h.2 h.1
    refine h (p.isMaximal.1.mono ?_)
    rw [insert_subset_iff, singleton_subset_iff]
    exact ⟨ht, hf⟩, (p.mem_or_not_mem φ).resolve_left⟩

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