Theorems · Theorem · logic and foundations
FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_ge
∀ (L : FirstOrder.Language) (M : Type w') [inst : L.Structure M] [iM : Infinite M] (κ : Cardinal.{w}),
Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ →
Cardinal.lift.{w, w'} (Cardinal.mk M) ≤ Cardinal.lift.{w', w} κ →
∃ N, Nonempty (L.ElementaryEmbedding M ↑N) ∧ Cardinal.mk ↑N = κThe Upward Löwenheim–Skolem Theorem: If κ is a cardinal greater than the cardinalities of
L and an infinite L-structure M, then M has an elementary extension of cardinality κ.
- Defined in
- Mathlib.ModelTheory.Satisfiability
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites36
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
- add_commproof · cited by 1,535
- FirstOrder.Languagestatement and proof · cited by 1,084
- Cardinal.mkstatement and proof · cited by 942
- FirstOrder.Language.Structurestatement and proof · cited by 775
- CategoryTheory.Bundled.αstatement and proof · cited by 736
- Cardinal.liftstatement and proof · cited by 583
- Infinitestatement and proof · cited by 352
- Cardinal.lift_idproof · cited by 163
- FirstOrder.Language.withConstantsproof · cited by 108
Cited by1
Results whose statement or proof uses this declaration.
- FirstOrder.Language.exists_elementaryEmbedding_card_eqproof · cited by 1