card_le_of_model_distinctConstantsTheory

English

If M models that the constants indexed by s are all distinct, then the (lifted) cardinality of s is at most the (lifted) cardinality of M.

Русский

Если структура M удовлетворяет теории, в которой константы с индексами из s попарно различны, то кардинальность s не превосходит кардинальности M (в поднятом кардинале).

LaTeX

$$M ⊨ L.distinctConstantsTheory s ⇒ lift #s ≤ lift #M$$

Lean4

theorem card_le_of_model_distinctConstantsTheory (s : Set α) (M : Type w) [L[[α]].Structure M]
    [h : M ⊨ L.distinctConstantsTheory s] : Cardinal.lift.{w} #s ≤ Cardinal.lift.{u'} #M :=
  lift_mk_le'.2 ⟨⟨_, Set.injOn_iff_injective.1 ((L.model_distinctConstantsTheory s).1 h)⟩⟩

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