realize_iff — Mathlib

English

If T proves φ ⇔ ψ, then in any model M, φ.Realize v equals ψ.Realize v for all v.

Русский

Если T доказывает φ ⇔ ψ, то в любой модели M при любых v выполняется φ.Realize v = ψ.Realize v.

LaTeX

$$$$ T.Iff(\varphi, \psi) \Rightarrow \forall v, \ \varphi.Realize v \iff \psi.Realize v $$$$

Lean4

theorem realize_iff {φ ψ : L.Formula α} {M : Type*} [Nonempty M] [L.Structure M] [M ⊨ T] (h : φ ⇔[T] ψ) {v : α → M} :
    φ.Realize v ↔ ψ.Realize v :=
  h.realize_bd_iff

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