models_sentence_iff — Mathlib

English

If φ ⇔ ψ modulo T, then for any model M, M ⊨ φ iff M ⊨ ψ.

Русский

Если φ ⇔ ψ по отношению к T, то для любой модели M выполняются φ и ψ одновременно (M ⊨ φ эквивалентно M ⊨ ψ).

LaTeX

$$$$ M \vDash \varphi \iff M \vDash \psi $$$$

Lean4

theorem models_sentence_iff {φ ψ : L.Sentence} {M : Type*} [Nonempty M] [L.Structure M] [M ⊨ T] (h : φ ⇔[T] ψ) :
    M ⊨ φ ↔ M ⊨ ψ :=
  h.realize_iff

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