Theorems · Theorem · logic and foundations

FirstOrder.Language.BoundedFormula.card_le

∀ {L : FirstOrder.Language} {α : Type u'},
  Cardinal.mk ((n : ℕ) × L.BoundedFormula α n) ≤
    max Cardinal.aleph0 (Cardinal.lift.{max u v, u'} (Cardinal.mk α) + Cardinal.lift.{u', max u v} L.card)

Defined in: Mathlib.ModelTheory.Encoding
Cited by: 1 results in Mathlib
Foundations: Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites30

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

LE.le.transproof · cited by 3,151
Cardinalstatement and proof · cited by 2,598
le_reflproof · cited by 2,061
le_rflproof · cited by 1,558
add_commproof · cited by 1,535
FirstOrder.Languagestatement and proof · cited by 1,084
Cardinal.mkstatement and proof · cited by 942
add_assocproof · cited by 746
Cardinal.liftstatement and proof · cited by 583
Cardinal.aleph0statement and proof · cited by 521
le_max_leftproof · cited by 215
FirstOrder.Language.BoundedFormulastatement · cited by 207

Cited by1

Results whose statement or proof uses this declaration.

FirstOrder.Language.card_functions_sum_skolem₁_leproof · cited by 1