castLE — Mathlib

English

Casting between bounded formulas is compatible with composition: casting from k to m and then from m to n equals casting directly from k to n (under the natural monotoneity assumption).

Русский

Преобразование индексов формул через castLE совместимо с композициями: каст к m а потом к n равно прямому касту к n.

LaTeX

$$$\forall {k\,m\,n} (km : k \le m) (mn : m \le n) (\varphi : L.BoundedFormula α k),\; (\varphi.castLE km).castLE mn = \varphi.castLE (km.tran s mn).$$$

Lean4

/-- Casts `L.BoundedFormula α m` as `L.BoundedFormula α n`, where `m ≤ n`. -/
@[simp]
def castLE : ∀ {m n : ℕ} (_h : m ≤ n), L.BoundedFormula α m → L.BoundedFormula α n
  | _m, _n, _h, falsum => falsum
  | _m, _n, h, equal t₁ t₂ => equal (t₁.relabel (Sum.map id (Fin.castLE h))) (t₂.relabel (Sum.map id (Fin.castLE h)))
  | _m, _n, h, rel R ts => rel R (Term.relabel (Sum.map id (Fin.castLE h)) ∘ ts)
  | _m, _n, h, imp f₁ f₂ => (f₁.castLE h).imp (f₂.castLE h)
  | _m, _n, h, all f => (f.castLE (add_le_add_right h 1)).all

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