instMembership — Mathlib

English

There is a Membership structure for Ordset α, i.e., a canonical relation ∈ between α and Ordset α is defined.

Русский

Для Ordset α существует структура принадлежности, то есть определено отношение ∈ между элементами типа α и Ordset α.

LaTeX

$$$$ \\in:\\alpha \\times \\mathrm{Ordset}(\\alpha) \\to \\mathbb{B}. $$$$

Lean4

instance instMembership : Membership α (Ordset α) :=
  ⟨fun s x => mem x s⟩

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