ex — Mathlib · SciLib

English

If φ ⇔ ψ, then φ.Realize and ψ.Realize are linked by Iff in any model.

Русский

Если φ ⇔ ψ, то их реализации связаны отношением эквивалентности в любой модели.

LaTeX

$$$$ \text{(φ.Realize)} \Leftrightarrow \text{(ψ.Realize)} $$$$

Lean4

protected theorem ex {φ ψ : L.BoundedFormula α (n + 1)} (h : φ ⇔[T] ψ) : φ.ex ⇔[T] ψ.ex :=
  by
  simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff, BoundedFormula.realize_ex]
  exact fun M v xs => exists_congr fun a => h.realize_bd_iff

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