sup_iff_not_inf_not

Mathlib.ModelTheory.Equivalence

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

English

Equivalence with lifting and universal quantification: φ ⇔ (liftAt 1 n φ).all.

Русский

Эквивалентность с поднятием и всеобщностью: φ ⇔ (liftAt 1 n φ).all.

LaTeX

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

Lean4

theorem sup_iff_not_inf_not : (φ ⊔ ψ) ⇔[T] (φ.not ⊓ ψ.not).not := fun M v xs => by simp [imp_iff_not_or]

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

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

Разделы

Аффилиация

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