instMembership

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#OmegaCompletePartialOrder.Chain.instMembership

English

An element a belongs to a chain c if and only if there exists i with a = c(i).

Русский

Элемент a принадлежит цепи c тогда, когда существует индекс i such that a = c(i).

LaTeX

$${ a ∈ c } := ∃ i, a = c(i).$$

Lean4

instance : Membership α (Chain α) :=
  ⟨fun (c : ℕ →o α) a => ∃ i, a = c i⟩

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

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

Разделы

Аффилиация

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