refl

Mathlib.ModelTheory.Equivalence

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Theory.Imp.refl

English

Any φ implies the top formula, which is universally true.

Русский

Любая формула φ следует из верхней формулы, которая истина по определению.

LaTeX

$$$T.Imp(φ, ⊤)$$$

Lean4

@[refl]
protected theorem refl (φ : L.BoundedFormula α n) : φ ⟹[T] φ := fun _ _ _ => id

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

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

Разделы

Аффилиация

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