liftAt — Mathlib

English

Lifting a bounded formula preserves atomicity: if φ is atomic, then φ.liftAt k m is atomic.

Русский

Перенос ограниченной формулы сохраняет атомарность: если φ атомарна, то φ.liftAt k m атомарна.

LaTeX

$$$\text{IsAtomic}(\phi) \Rightarrow \text{IsAtomic}(\phi\mathrm{.liftAt}\;k\;m)$$$

Lean4

theorem liftAt {k m : ℕ} (h : IsAtomic φ) : (φ.liftAt k m).IsAtomic :=
  IsAtomic.recOn h (fun _ _ => IsAtomic.equal _ _) fun _ _ => IsAtomic.rel _ _

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