relabel — Mathlib

English

If φ is atomic, then relabeling preserves atomicity for any relabeling map.

Русский

Если φ атомарна, то перенос левых переменных на другую структуру сохраняет атомарность.

LaTeX

$$$\forall {L} {M} {\alpha} {\beta} {n} {m} (\varphi : L.BoundedFormula \alpha m), \varphi.IsAtomic \rightarrow \forall f : \alpha \to (\beta \oplus (\mathrm{Fin}~n)), (\varphi.relabel f).IsAtomic.$$$

Lean4

theorem relabel {m : ℕ} {φ : L.BoundedFormula α m} (h : φ.IsAtomic) (f : α → β ⊕ (Fin n)) : (φ.relabel f).IsAtomic :=
  IsAtomic.recOn h (fun _ _ => IsAtomic.equal _ _) fun _ _ => IsAtomic.rel _ _

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