iff_all_liftAt

Mathlib.ModelTheory.Equivalence

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.BoundedFormula.iff_all_liftAt

English

Equivalence under T between φ and its lifted form followed by all.

Русский

Эквивалентность по отношению к T между φ и его поднимаемой формой, затем все.

LaTeX

$$$$ \varphi \iff_T (\varphi.liftAt 1 n).all $$$$

Lean4

theorem iff_all_liftAt : φ ⇔[T] (φ.liftAt 1 n).all := fun M v xs => by rw [realize_iff, realize_all_liftAt_one_self]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru