instIsEmptySubtypeMemBotOfConstants

English

If the language has no constant symbols, the bottom substructure of M is empty.

Русский

Если язык не содержит констант, младшая подструктура множества M пустая.

LaTeX

$$$\\operatorname{IsEmpty}(\\bot : L\\text{-Substructure } M)$$$

Lean4

instance [IsEmpty L.Constants] : IsEmpty (⊥ : L.Substructure M) :=
  by
  refine (isEmpty_subtype _).2 (fun x => ?_)
  have h : (∅ : Set M) ∈ (closure L).closed := by
    rw [mem_closed_iff]
    intro n f
    cases n
    · exact isEmptyElim f
    · intro x hx
      simp only [mem_empty_iff_false, forall_const] at hx
  rw [← closure_empty, ← SetLike.mem_coe, h]
  exact Set.notMem_empty _

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