Theorems · Theorem · logic and foundations

FirstOrder.Language.BoundedFormula.castLE_castLE

∀ {L : FirstOrder.Language} {α : Type u'} {k m n : ℕ} (km : k ≤ m) (mn : m ≤ n) (φ : L.BoundedFormula α k),
  FirstOrder.Language.BoundedFormula.castLE mn (FirstOrder.Language.BoundedFormula.castLE km φ) =
    FirstOrder.Language.BoundedFormula.castLE ⋯ φ

Defined in: Mathlib.ModelTheory.Syntax
Cited by: 1 results in Mathlib
Foundations: Depth 26 from the axioms · uses propext, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

LE.le.transstatement and proof · cited by 3,151
FirstOrder.Languagestatement and proof · cited by 1,084
FirstOrder.Language.BoundedFormulastatement and proof · cited by 207
FirstOrder.Language.Termproof · cited by 166
FirstOrder.Language.Relationsproof · cited by 147
Function.comp_assocproof · cited by 41
FirstOrder.Language.Term.relabelproof · cited by 27
FirstOrder.Language.BoundedFormula.castLEstatement and proof · cited by 13
FirstOrder.Language.Term.relabel_relabelproof · cited by 3
FirstOrder.Language.Term.relabel_comp_relabelproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

FirstOrder.Language.BoundedFormula.castLE_comp_castLEproof · cited by 0