instUniqueSymbols

Mathlib.ModelTheory.Order

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.order.instUniqueSymbols

← MathLib Explorer

English

The cardinality of Language.order.card equals 1.

Русский

Кардинал Language.order.card равен 1.

LaTeX

$$$ \\operatorname{card}(Language.order) = 1 $$$

Lean4

instance : Unique Language.order.Symbols :=
  ⟨⟨Sum.inr default⟩,
    by
    have : IsEmpty (Σ n, Language.order.Functions n) := isEmpty_sigma.2 inferInstance
    simp only [Symbols, Sum.forall, reduceCtorEq, Sum.inr.injEq, IsEmpty.forall_iff, true_and]
    exact Unique.eq_default⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru